1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Sébastien Gouëzel
  5  -/
  6  
  7  import topology.metric_space.hausdorff_distance topology.opens analysis.specific_limits
src         └──────────────────────────────────────┘ └────────────┘ └──────────────────────┘
  8  
  9  /-!
 10  # Closed subsets
 11  
 12  This file defines the metric and emetric space structure on the types of closed subsets and nonempty compact
 13  subsets of a metric or emetric space.
 14  
 15  The Hausdorff distance induces an emetric space structure on the type of closed subsets
 16  of an emetric space, called `closeds`. Its completeness, resp. compactness, resp.
 17  second-countability, follow from the corresponding properties of the original space.
 18  
 19  In a metric space, the type of nonempty compact subsets (called `nonempty_compacts`) also
 20  inherits a metric space structure from the Hausdorff distance, as the Hausdorff edistance is
 21  always finite in this context.
 22  -/
 23  
 24  noncomputable theory
 25  open_locale classical
 26  open_locale topological_space
 27  
 28  universe u
 29  open classical lattice set function topological_space filter
 30  
 31  namespace emetric
 32  section
 33  variables {α : Type u} [emetric_space α] {s : set α}
id                           └───────────┘         └─┘
src                          └───────────┘         └─┘
typ                          └───────────┘         └─┘
doc                          └───────────┘
 34  
 35  /-- In emetric spaces, the Hausdorff edistance defines an emetric space structure
 36  on the type of closed subsets -/
 37  instance closeds.emetric_space : emetric_space (closeds α) :=
id                                    └───────────┘  └─────┘ 
src                                   └───────────┘  └─────┘
typ                                   └───────────┘  └─────┘ 
doc                                   └───────────┘  └─────┘
 38  { edist               := λs t, Hausdorff_edist s.val t.val,
id                               └─────────────┘ └──┘ └──┘
src                                └─────────────┘  └──┘  └──┘
typ                              └─────────────┘ └──┘ └──┘
doc                                 └─────────────┘
 39    edist_self          := λs, Hausdorff_edist_self,
id                               └──────────────────┘
src                               └──────────────────┘
typ                              └──────────────────┘
doc                               └──────────────────┘
 40    edist_comm          := λs t, Hausdorff_edist_comm,
id                                └──────────────────┘
src                                 └──────────────────┘
typ                               └──────────────────┘
doc                                 └──────────────────┘
 41    edist_triangle      := λs t u, Hausdorff_edist_triangle,
id                                 └──────────────────────┘
src                                   └──────────────────────┘
typ                                └──────────────────────┘
doc                                   └──────────────────────┘
 42    eq_of_edist_eq_zero :=
 43      λs t h, subtype.eq ((Hausdorff_edist_zero_iff_eq_of_closed s.property t.property).1 h) }
id            └────────┘   └───────────────────────────────────┘ └───────┘ └───────┘   
src              └────────┘   └───────────────────────────────────┘  └───────┘  └───────┘ 
typ           └────────┘   └───────────────────────────────────┘ └───────┘ └───────┘   
doc                           └───────────────────────────────────┘
 44  
 45  /-- The edistance to a closed set depends continuously on the point and the set -/
 46  lemma continuous_inf_edist_Hausdorff_edist :
 47    continuous (λp : α × (closeds α), inf_edist p.1 (p.2).val) :=
id     └────────┘          └─────┘    └───────┘      └─┘
src    └────────┘           └─────┘     └───────┘        └─┘
typ    └────────┘          └─────┘    └───────┘      └─┘
doc    └────────┘            └─────┘     └───────┘
 48  begin
st   └─────
 49    refine continuous_of_le_add_edist 2 (by simp) _,
id            └────────────────────────┘
src    └─────┘└────────────────────────┘└─┘   └──┘└─┘
typ    └─────┘└────────────────────────┘└─┘   └──┘└─┘
doc    └─────┘                          └─┘   └──┘└─┘
txt    └─────┘                          └─┘   └──┘└─┘
par    └─────┘                          └─┘   └──┘└─┘
pid                                    └─┘   └──────┘
st   ────────────────────────────────────────┘└───┘└─┘└─
 50    rintros ⟨x, s⟩ ⟨y, t⟩,
src    └───────────────────┘
typ    └───────────────────┘
doc    └───────────────────┘
txt    └───────────────────┘
par    └───────────────────┘
pid           └────────────┘
st   ──────────────────────┘└─
 51    calc inf_edist x (s.val) ≤ inf_edist x (t.val) + Hausdorff_edist (t.val) (s.val) :
id     └──┘                       └───────┘            └─────────────┘  └───┘   └───┘
src    └──┘                       └───────┘             └─────────────┘  └───┘   └───┘
typ    └──┘                       └───────┘            └─────────────┘  └───┘   └───┘
doc    └──┘                       └───────┘             └─────────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────
 52      inf_edist_le_inf_edist_add_Hausdorff_edist
id       └────────────────────────────────────────┘
src      └────────────────────────────────────────┘
typ      └────────────────────────────────────────┘
doc      └────────────────────────────────────────┘
st   ───────────────────────────────────────────────
 53    ... ≤ (inf_edist y (t.val) + edist x y) + Hausdorff_edist (t.val) (s.val) :
id                                  └───┘   
src                                 └───┘
typ                                 └───┘   
st   ──────────────────────────────────────────────────────────────────────────────
 54      add_le_add_right' inf_edist_le_inf_edist_add_edist
id       └───────────────┘ └──────────────────────────────┘
src      └───────────────┘ └──────────────────────────────┘
typ      └───────────────┘ └──────────────────────────────┘
doc                        └──────────────────────────────┘
st   ───────────────────────────────────────────────────────
 55    ... = inf_edist y (t.val) + (edist x y + Hausdorff_edist (s.val) (t.val)) :
st   ──────────────────────────────────────────────────────────────────────────────
 56      by simp [add_comm, Hausdorff_edist_comm]
id                └──────┘  └──────────────────┘
src         └────┘└──────┘└┘└──────────────────┘└─
typ         └────┘└──────┘└┘└──────────────────┘└─
doc         └────┘        └┘└──────────────────┘└─
txt         └────┘        └┘                    └─
par         └────┘        └┘                    └─
pid                     └┘                    
st   ─────┘└──────────────────────────────────────
 57    ... ≤ inf_edist y (t.val) + (edist (x, s) (y, t) + edist (x, s) (y, t)) :
id                                       
src  ─┘                                  
typ  ─┘                                  
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─────────────────────────────────────────────────────────────────────────
 58      add_le_add_left' (add_le_add' (by simp [edist, le_refl]) (by simp [edist, le_refl]))
id       └──────────────┘  └─────────┘                  └─────┘                    └─────┘
src      └──────────────┘  └─────────┘     └────┘     └┘└─────┘      └────┘     └┘└─────┘
typ      └──────────────┘  └─────────┘     └────┘     └┘└─────┘      └────┘     └┘└─────┘
doc                                        └────┘     └┘             └────┘     └┘       
txt                                        └────┘     └┘             └────┘     └┘       
par                                        └────┘     └┘             └────┘     └┘       
pid                                                 └┘                      └┘       
st   ────────────────────────────────────┘└────────────────────┘└───┘└────────────────────┘└──
 59    ... = inf_edist y (t.val) + 2 * edist (x, s) (y, t) :
id                                   
src                                  
typ                                  
st   ────────────────────────────────────────────────────────
 60      by rw [← mul_two, mul_comm]
id                └─────┘  └──────┘
src         └────┘└─────┘└┘└──────┘└┘
typ         └────┘└─────┘└┘└──────┘└┘
doc         └────┘       └┘        └┘
txt         └────┘       └┘        └┘
par         └────┘       └┘        └┘
pid           └──┘       └┘        
st   ─────┘└────────────┘└────────┘
 61  end
st   └─┘
 62  
 63  /-- Subsets of a given closed subset form a closed set -/
 64  lemma is_closed_subsets_of_is_closed (hs : is_closed s) :
id                                              └───────┘ 
src                                             └───────┘
typ                                             └───────┘ 
doc                                             └───────┘
 65    is_closed {t : closeds α | t.val ⊆ s} :=
id     └───────┘     └─────┘    └──┘  
src    └───────┘     └─────┘      └──┘ 
typ    └───────┘     └─────┘    └──┘  
doc    └───────┘      └─────┘
 66  begin
st   └─────
 67    refine is_closed_of_closure_subset (λt ht x hx, _),
id            └─────────────────────────┘
src    └─────┘└─────────────────────────┘  └───────────┘
typ    └─────┘└─────────────────────────┘  └───────────┘
doc    └─────┘                             └───────────┘
txt    └─────┘                             └───────────┘
par    └─────┘                             └───────────┘
pid                                       └───────────┘
st   ───────────────────────────────────────────────────┘└─
 68    -- t : closeds α,  ht : t ∈ closure {t : closeds α | t.val ⊆ s},
st   ───────────────────────────────────────────────────────────────────
 69    -- x : α,  hx : x ∈ t.val
st   ────────────────────────────
 70    -- goal : x ∈ s
st   ──────────────────
 71    have : x ∈ closure s,
id              └─────┘ 
src    └─────┘ └─────┘
typ    └─────┘└─────┘
doc    └─────┘  └─────┘
txt    └─────┘         
par    └─────┘         
pid    └───┘└┘         
st   ─────────────────────┘└─
 72    { refine mem_closure_iff'.2 (λε εpos, _),
id              └──────────────┘
src      └─────┘└──────────────┘└─┘  └────────┘
typ      └─────┘└──────────────┘└─┘  └────────┘
doc      └─────┘└──────────────┘└─┘  └────────┘
txt      └─────┘                └─┘  └────────┘
par      └─────┘                └─┘  └────────┘
pid                            └─┘  └────────┘
st   ───┘└────────────────────────────────────┘└─
 73      rcases mem_closure_iff'.1 ht ε εpos with ⟨u, hu, Dtu⟩,
id              └──────────────┘   └┘  └──┘
src      └─────┘└──────────────┘└─┘       └────────────────┘
typ      └─────┘└──────────────┘└─┘└┘└──┘└────────────────┘
doc      └─────┘└──────────────┘└─┘       └────────────────┘
txt      └─────┘                └─┘       └────────────────┘
par      └─────┘                └─┘       └────────────────┘
pid                            └─┘       └────────────────┘
st   ────────────────────────────────────────────────────────┘└─
 74      -- u : closeds α,  hu : u ∈ {t : closeds α | t.val ⊆ s},  hu' : edist t u < ε
st   ──────────────────────────────────────────────────────────────────────────────────
 75      rcases exists_edist_lt_of_Hausdorff_edist_lt hx Dtu with ⟨y, hy, Dxy⟩,
id              └───────────────────────────────────┘ └┘ └─┘
src      └─────┘└───────────────────────────────────┘     └────────────────┘
typ      └─────┘└───────────────────────────────────┘└┘└─┘└────────────────┘
doc      └─────┘└───────────────────────────────────┘     └────────────────┘
txt      └─────┘                                          └────────────────┘
par      └─────┘                                          └────────────────┘
pid                                                      └────────────────┘
st   ────────────────────────────────────────────────────────────────────────┘└─
 76      -- y : α,  hy : y ∈ u.val, Dxy : edist x y < ε
st   ───────────────────────────────────────────────────
 77      exact ⟨y, hu hy, Dxy⟩ },
id                └┘ └┘  └─┘
src      └────┘  └┘    └┘   └┘
typ      └────┘ └┘└┘└┘└┘└─┘└┘
doc      └────┘  └┘    └┘   └┘
txt      └────┘  └┘    └┘   └┘
par      └────┘  └┘    └┘   └┘
pid             └┘    └┘   
st   ─────────────────────────┘└┘
 78    rwa closure_eq_of_is_closed hs at this,
id         └─────────────────────┘ └┘
src    └──┘└─────────────────────┘  └──────┘
typ    └──┘└─────────────────────┘└┘└──────┘
doc    └──┘                         └──────┘
txt    └──┘                         └──────┘
par    └──┘                         └──────┘
pid                                └──────┘
st   ───────────────────────────────────────┘└─
 79  end
st   ──┘
 80  
 81  /-- By definition, the edistance on `closeds α` is given by the Hausdorff edistance -/
 82  lemma closeds.edist_eq {s t : closeds α} : edist s t = Hausdorff_edist s.val t.val := rfl
id                                 └─────┘     └───┘    └─────────────┘ └──┘ └──┘    └─┘
src                                └─────┘      └───┘      └─────────────┘  └──┘  └──┘    └─┘
typ                                └─────┘     └───┘    └─────────────┘ └──┘ └──┘    └─┘
doc                                └─────┘                  └─────────────┘
 83  
 84  /-- In a complete space, the type of closed subsets is complete for the
 85  Hausdorff edistance. -/
 86  instance closeds.complete_space [complete_space α] : complete_space (closeds α) :=
id                                    └────────────┘     └────────────┘  └─────┘ 
src                                   └────────────┘      └────────────┘  └─────┘
typ                                   └────────────┘     └────────────┘  └─────┘ 
doc                                   └────────────┘      └────────────┘  └─────┘
 87  begin
st   └─────
 88    /- We will show that, if a sequence of sets `s n` satisfies
st   ──────────────────────────────────────────────────────────────
 89    `edist (s n) (s (n+1)) < 2^{-n}`, then it converges. This is enough to guarantee
st   ───────────────────────────────────────────────────────────────────────────────────
 90    completeness, by a standard completeness criterion.
st   ──────────────────────────────────────────────────────
 91    We use the shorthand `B n = 2^{-n}` in ennreal. -/
st   ─────────────────────────────────────────────────────
 92    let B : ℕ → ennreal := λ n, (2⁻¹)^n,
id                 └─────┘           └┘ 
src    └──────┘  └─────┘└──┘ └──┘ └┘
typ    └──────┘  └─────┘└──┘ └──┘ └┘
doc    └──────┘  └─────┘└──┘ └──┘   
txt    └──────┘         └──┘ └──┘   
par    └──────┘         └──┘ └──┘   
pid    └───┘└─┘         └──┘ └──┘   
st   ────────────────────────────────────┘└─
 93    have B_pos : ∀ n, (0:ennreal) < B n,
id                          └─────┘   
src    └───────────┘ └┘  └┘└─────┘└┘ 
typ    └───────────┘ └┘  └┘└─────┘└┘
doc    └───────────┘ └┘  └┘└─────┘└┘  
txt    └───────────┘ └┘  └┘       └┘  
par    └───────────┘ └┘  └┘       └┘  
pid    └────────┘└─┘ └┘  └┘       └┘  
st   ────────────────────────────────────┘
 94      by simp [B, ennreal.pow_pos],
id                  └─────────────┘
src         └────┘ └┘└─────────────┘
typ         └────┘└┘└─────────────┘
doc         └────┘ └┘               
txt         └────┘ └┘               
par         └────┘ └┘               
pid              └┘               
st                                   └─
 95    have B_ne_top : ∀ n, B n ≠ ⊤,
id                              
src    └──────────────┘ └┘   
typ    └──────────────┘ └┘  
doc    └──────────────┘ └┘    
txt    └──────────────┘ └┘    
par    └──────────────┘ └┘    
pid    └───────────┘└─┘ └┘    
st   ─────────────────────────────┘
 96      by simp [B, ennreal.div_def, ennreal.pow_ne_top],
id                  └─────────────┘  └────────────────┘
src         └────┘ └┘└─────────────┘└┘└────────────────┘
typ         └────┘└┘└─────────────┘└┘└────────────────┘
doc         └────┘ └┘               └┘                  
txt         └────┘ └┘               └┘                  
par         └────┘ └┘               └┘                  
pid              └┘               └┘                  
st                                                       └─
 97    /- Consider a sequence of closed sets `s n` with `edist (s n) (s (n+1)) < B n`.
st   ──────────────────────────────────────────────────────────────────────────────────
 98    We will show that it converges. The limit set is t0 = ⋂n, closure (⋃m≥n, s m).
st   ─────────────────────────────────────────────────────────────────────────────────
 99    We will have to show that a point in `s n` is close to a point in `t0`, and a point
st   ──────────────────────────────────────────────────────────────────────────────────────
100    in `t0` is close to a point in `s n`. The completeness then follows from a
st   ─────────────────────────────────────────────────────────────────────────────
101    standard criterion. -/
st   ─────────────────────────
102    refine complete_of_convergent_controlled_sequences B B_pos (λs hs, _),
id            └─────────────────────────────────────────┘  └───┘
src    └─────┘└─────────────────────────────────────────┘        └──────┘
typ    └─────┘└─────────────────────────────────────────┘└───┘  └──────┘
doc    └─────┘└─────────────────────────────────────────┘        └──────┘
txt    └─────┘                                                   └──────┘
par    └─────┘                                                   └──────┘
pid                                                             └──────┘
st   ──────────────────────────────────────────────────────────────────────┘└─
103    let t0 := ⋂n, closure (⋃m≥n, (s m).val),
id                 └─────┘       
src    └────────┘└─────┘ └┘    └────┘
typ    └────────┘└─────┘ └┘   └────┘
doc    └────────┘└─────┘ └┘    └────┘
txt    └────────┘           └┘     └────┘
par    └────────┘           └┘     └────┘
pid    └────┘└─┘           └┘     └────┘
st   ────────────────────────────────────────┘└─
104    let t : closeds α := ⟨t0, is_closed_Inter (λ_, is_closed_closure)⟩,
id             └─────┘      └┘  └─────────────┘      └───────────────┘
src    └──────┘└─────┘ └──┘   └┘└─────────────┘  └─┘└───────────────┘└┘
typ    └──────┘└─────┘└──┘ └┘└┘└─────────────┘  └─┘└───────────────┘└┘
doc    └──────┘└─────┘ └──┘   └┘                 └─┘                 └┘
txt    └──────┘        └──┘   └┘                 └─┘                 └┘
par    └──────┘        └──┘   └┘                 └─┘                 └┘
pid    └───┘└─┘        └──┘   └┘                 └─┘                 └┘
st   ───────────────────────────────────────────────────────────────────┘└─
105    use t,
id         
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
pid       
st   ──────┘└─
106    -- The inequality is written this way to agree with `edist_le_of_edist_le_geometric_of_tendsto₀`
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
107    have I1 : ∀n:ℕ, ∀x ∈ (s n).val, ∃y ∈ t0, edist x y ≤ 2 * B n,
id                                        └┘ └───┘         
src    └────────┘ └┘   └──┘   └───┘ └──┘  └───┘  └─┘ 
typ    └────────┘ └┘   └──┘  └───┘ └──┘└┘└───┘  └─┘
doc    └────────┘ └┘   └──┘   └───┘  └──┘           └─┘  
txt    └────────┘ └┘   └──┘   └───┘  └──┘           └─┘  
par    └────────┘ └┘   └──┘   └───┘  └──┘           └─┘  
pid    └─────┘└─┘ └┘   └──┘   └───┘  └──┘           └─┘  
st   ─────────────────────────────────────────────────────────────┘└─
108    { /- This is the main difficulty of the proof. Starting from `x ∈ s n`, we want
st   ───┘└─────────────────────────────────────────────────────────────────────────────
109         to find a point in `t0` which is close to `x`. Define inductively a sequence of
st   ───────────────────────────────────────────────────────────────────────────────────────
110         points `z m` with `z n = x` and `z m ∈ s m` and `edist (z m) (z (m+1)) ≤ B m`. This is
st   ──────────────────────────────────────────────────────────────────────────────────────────────
111         possible since the Hausdorff distance between `s m` and `s (m+1)` is at most `B m`.
st   ───────────────────────────────────────────────────────────────────────────────────────────
112         This sequence is a Cauchy sequence, therefore converging as the space is complete, to
st   ─────────────────────────────────────────────────────────────────────────────────────────────
113         a limit which satisfies the required properties. -/
st   ───────────────────────────────────────────────────────────
114      assume n x hx,
src      └───────────┘
typ      └───────────┘
doc      └───────────┘
txt      └───────────┘
par      └───────────┘
pid      └───────────┘
st   ────────────────┘└─
115      obtain ⟨z, hz₀, hz⟩ : ∃ z : Π l, (s (n+l)).val, (z 0:α) = x ∧
id                                                             
src      └────────────────────┘└───┘ └┘      └────┘  └─┘ └┘ 
typ      └────────────────────┘└───┘ └┘     └────┘  └─┘ └┘
doc      └────────────────────┘ └───┘ └┘       └────┘   └─┘ └┘   
txt      └────────────────────┘ └───┘ └┘       └────┘   └─┘ └┘   
par      └────────────────────┘ └───┘ └┘       └────┘   └─┘ └┘   
pid            └──────────────┘ └───┘ └┘       └────┘   └─┘ └┘   
st   ──────────────────────────────────────────────────────────────────
116        ∀ k, edist (z k:α) (z (k+1):α) ≤ B n / 2^k,
id              └───┘                        
src  ─────┘ └┘ └───┘    └┘     └─┘ └┘   └┘
typ  ─────┘ └┘ └───┘    └┘     └─┘└┘ └┘
doc  ─────┘ └┘          └┘     └─┘ └┘    └┘
txt  ─────┘ └┘          └┘     └─┘ └┘    └┘
par  ─────┘ └┘          └┘     └─┘ └┘    └┘
pid  ─────┘ └┘          └┘     └─┘ └┘    └┘
st   ───────────────────────────────────────────────┘└─
117      { -- We prove existence of the sequence by induction.
st   ─────┘└───────────────────────────────────────────────────
118        have : ∀ (l : ℕ) (z : (s (n+l)).val), ∃ z' : (s (n+l+1)).val, edist (z:α) z' ≤ B n / 2^l,
id                                                                    └───┘            
src        └─────┘ └────┘ └─────┘      └─────┘ └────┘       └─────┘└───┘   └┘      └┘
typ        └─────┘ └────┘ └─────┘      └─────┘ └────┘      └─────┘└───┘  └┘    └┘
doc        └─────┘ └────┘ └─────┘      └─────┘  └────┘       └─────┘         └┘      └┘
txt        └─────┘ └────┘ └─────┘      └─────┘  └────┘       └─────┘         └┘      └┘
par        └─────┘ └────┘ └─────┘      └─────┘  └────┘       └─────┘         └┘      └┘
pid        └───┘└┘ └────┘ └─────┘      └─────┘  └────┘       └─────┘         └┘      └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘└─
119        { assume l z,
src          └────────┘
typ          └────────┘
doc          └────────┘
txt          └────────┘
par          └────────┘
pid          └────────┘
st   ───────┘└────────┘└─
120          obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ (s (n+l+1)).val, edist (z:α) z' < B n / 2^l,
id                                                           └───┘                
src          └─────────────────────────┘└────┘       └─────┘└───┘   └┘      └┘
typ          └─────────────────────────┘└────┘      └─────┘└───┘ └┘    └┘ 
doc          └─────────────────────────┘ └────┘       └─────┘         └┘      └┘
txt          └─────────────────────────┘ └────┘       └─────┘         └┘      └┘
par          └─────────────────────────┘ └────┘       └─────┘         └┘      └┘
pid                └───────────────────┘ └────┘       └─────┘         └┘      └┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
121          { apply exists_edist_lt_of_Hausdorff_edist_lt z.2,
id                   └───────────────────────────────────┘ 
src            └────┘└───────────────────────────────────┘ └┘
typ            └────┘└───────────────────────────────────┘└┘
doc            └────┘└───────────────────────────────────┘ └┘
txt            └────┘                                      └┘
par            └────┘                                      └┘
pid                                                       └┘
st   ─────────┘└─────────────────────────────────────────────┘└─
122            simp only [B, ennreal.div_def, ennreal.inv_pow'],
id                          └─────────────┘  └──────────────┘
src            └─────────┘ └┘└─────────────┘└┘└──────────────┘
typ            └─────────┘└┘└─────────────┘└┘└──────────────┘
doc            └─────────┘ └┘               └┘                
txt            └─────────┘ └┘               └┘                
par            └─────────┘ └┘               └┘                
pid                └──┘└┘ └┘               └┘                
st   ─────────────────────────────────────────────────────────┘└─
123            rw [← pow_add],
id                   └─────┘
src            └────┘└─────┘
typ            └────┘└─────┘
doc            └────┘       
txt            └────┘       
par            └────┘       
pid              └──┘       
st   ──────────────────────┘└──
124            apply hs; simp },
src            └────┘    └───┘
typ            └────┘    └───┘
doc            └────┘    └───┘
txt            └────┘    └───┘
par            └────┘    └───┘
pid                         
st   ────────────────────────┘└┘
125          exact ⟨⟨z', z'_mem⟩, le_of_lt hz'⟩ },
id                   └┘  └────┘   └──────┘ └─┘
src          └────┘    └┘      └─┘└──────┘   └┘
typ          └────┘  └┘└┘└────┘└─┘└──────┘└─┘└┘
doc          └────┘    └┘      └─┘           └┘
txt          └────┘    └┘      └─┘           └┘
par          └────┘    └┘      └─┘           └┘
pid                   └┘      └─┘           
st   ──────────────────────────────────────────┘└┘
126        use [λ k, nat.rec_on k ⟨x, hx⟩ (λl z, some (this l z)), rfl],
id                   └────────┘      └┘         └──┘  └──┘        └─┘
src        └───┘ └──┘└────────┘   └┘  └┘  └───┘└──┘       └──┘└─┘
typ        └───┘ └──┘└────────┘  └┘└┘└┘  └───┘└──┘ └──┘  └──┘└─┘
doc        └───┘ └──┘             └┘  └┘  └───┘           └──┘   
txt        └───┘ └──┘             └┘  └┘  └───┘           └──┘   
par        └───┘ └──┘             └┘  └┘  └───┘           └──┘   
pid           └┘ └──┘             └┘  └┘  └───┘           └──┘   
st   ─────────────────────────────────────────────────────────────────┘└─
127        exact λ k, some_spec (this k _) },
id                    └───────┘  └──┘
src        └────┘ └──┘└───────┘      └──┘
typ        └────┘ └──┘└───────┘ └──┘ └──┘
doc        └────┘ └──┘               └──┘
txt        └────┘ └──┘               └──┘
par        └────┘ └──┘               └──┘
pid              └──┘               └─┘
st   ─────────────────────────────────────┘└┘
128      -- it follows from the previous bound that `z` is a Cauchy sequence
st   ────────────────────────────────────────────────────────────────────────
129      have : cauchy_seq (λ k, ((z k):α)),
id              └────────┘             
src      └─────┘└────────┘  └──┘    └┘ └┘
typ      └─────┘└────────┘  └──┘   └┘└┘
doc      └─────┘└────────┘  └──┘    └┘ └┘
txt      └─────┘            └──┘    └┘ └┘
par      └─────┘            └──┘    └┘ └┘
pid      └───┘└┘            └──┘    └┘ └┘
st   ─────────────────────────────────────┘└─
130        from cauchy_seq_of_edist_le_geometric_two (B n) (B_ne_top n) hz,
id              └──────────────────────────────────┘       └──────┘   └┘
src        └───┘└──────────────────────────────────┘   └┘          └┘
typ        └───┘└──────────────────────────────────┘  └┘ └──────┘└┘└┘
doc        └───┘└──────────────────────────────────┘   └┘          └┘
txt        └───┘                                       └┘          └┘
par        └───┘                                       └┘          └┘
pid        └───┘                                       └┘          └┘
st   ────────────────────────────────────────────────────────────────────┘└─
131      -- therefore, it converges
st   ───────────────────────────────
132      rcases cauchy_seq_tendsto_of_complete this with ⟨y, y_lim⟩,
id              └────────────────────────────┘ └──┘
src      └─────┘└────────────────────────────┘    └──────────────┘
typ      └─────┘└────────────────────────────┘└──┘└──────────────┘
doc      └─────┘└────────────────────────────┘    └──────────────┘
txt      └─────┘                                  └──────────────┘
par      └─────┘                                  └──────────────┘
pid                                              └──────────────┘
st   ─────────────────────────────────────────────────────────────┘└─
133      use y,
id           
src      └──┘
typ      └──┘
doc      └──┘
txt      └──┘
par      └──┘
pid         
st   ────────┘└─
134      -- the limit point `y` will be the desired point, in `t0` and close to our initial point `x`.
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
135      -- First, we check it belongs to `t0`.
st   ───────────────────────────────────────────
136      have : y ∈ t0 := mem_Inter.2 (λk, mem_closure_of_tendsto (by simp) y_lim
id                 └┘    └───────┘        └────────────────────┘           └───┘
src      └─────┘    └──┘└───────┘└─┘  └─┘└────────────────────┘   └──┘└┘     
typ      └─────┘ └┘└──┘└───────┘└─┘  └─┘└────────────────────┘   └──┘└┘└───┘
doc      └─────┘    └──┘         └─┘  └─┘                         └──┘└┘     
txt      └─────┘    └──┘         └─┘  └─┘                         └──┘└┘     
par      └─────┘    └──┘         └─┘  └─┘                         └──┘└┘     
pid      └───┘└┘    └──┘         └─┘  └─┘                         └─────┘     
st   ───────────────────────────────────────────────────────────────┘└───┘└───────
137      begin
src  ───┘     
typ  ───┘     
doc  ───┘     
txt  ───┘     
par  ───┘     
pid  ───┘     
st   ───┘└─────
138        simp only [exists_prop, set.mem_Union, filter.mem_at_top_sets, set.mem_preimage, set.preimage_Union],
id                    └─────────┘  └───────────┘  └────────────────────┘  └──────────────┘  └────────────────┘
src  ─────┘└─────────┘└─────────┘└┘└───────────┘└┘└────────────────────┘└┘└──────────────┘└┘└────────────────┘└─
typ  ─────┘└─────────┘└─────────┘└┘└───────────┘└┘└────────────────────┘└┘└──────────────┘└┘└────────────────┘└─
doc  ─────┘└─────────┘           └┘             └┘                      └┘                └┘                  └─
txt  ─────┘└─────────┘           └┘             └┘                      └┘                └┘                  └─
par  ─────┘└─────────┘           └┘             └┘                      └┘                └┘                  └─
pid  ────────────────┘           └┘             └┘                      └┘                └┘                  └──
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
139        exact ⟨k, λ m hm, ⟨n+m, zero_add k ▸ add_le_add (zero_le n) hm, (z m).2⟩⟩
id                                 └──────┘   └────────┘  └─────┘        
src  ─────┘└────┘  └┘ └─────┘    └┘└──────┘ └────────┘ └─────┘ └┘  └┘   └─────
typ  ─────┘└────┘  └┘ └─────┘    └┘└──────┘└────────┘ └─────┘└┘  └┘  └─────
doc  ─────┘└────┘  └┘ └─────┘    └┘                             └┘  └┘   └─────
txt  ─────┘└────┘  └┘ └─────┘    └┘                             └┘  └┘   └─────
par  ─────┘└────┘  └┘ └─────┘    └┘                             └┘  └┘   └─────
pid  ───────────┘  └┘ └─────┘    └┘                             └┘  └┘   └─────
st   ────────────────────────────────────────────────────────────────────────────────
140      end),
src  ───┘└──┘
typ  ───┘└──┘
doc  ───┘└──┘
txt  ───┘└──┘
par  ───┘└──┘
pid  ───────┘
st   ───┘└─┘└─
141      use this,
id           └──┘
src      └──┘
typ      └──┘└──┘
doc      └──┘
txt      └──┘
par      └──┘
pid         
st   ───────────┘└─
142      -- Then, we check that `y` is close to `x = z n`. This follows from the fact that `y`
st   ──────────────────────────────────────────────────────────────────────────────────────────
143      -- is the limit of `z k`, and the distance between `z n` and `z k` has already been estimated.
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
144      rw [← hz₀],
id             └─┘
src      └────┘   
typ      └────┘└─┘
doc      └────┘   
txt      └────┘   
par      └────┘   
pid        └──┘   
st   ────────────┘└──
145      exact edist_le_of_edist_le_geometric_two_of_tendsto₀ (B n) hz y_lim },
id             └────────────────────────────────────────────┘     └┘ └───┘
src      └────┘└────────────────────────────────────────────┘   └┘       
typ      └────┘└────────────────────────────────────────────┘ └┘└┘└───┘
doc      └────┘└────────────────────────────────────────────┘   └┘       
txt      └────┘                                                 └┘       
par      └────┘                                                 └┘       
pid                                                            └┘       
st   ───────────────────────────────────────────────────────────────────────┘└┘
146    have I2 : ∀n:ℕ, ∀x ∈ t0, ∃y ∈ (s n).val, edist x y ≤ 2 * B n,
id                          └┘               └───┘           
src    └────────┘ └┘   └──┘   └──┘   └───┘└───┘   └─┘  
typ    └────────┘ └┘   └──┘└┘ └──┘  └───┘└───┘   └─┘ 
doc    └────────┘ └┘   └──┘    └──┘   └───┘         └─┘  
txt    └────────┘ └┘   └──┘    └──┘   └───┘         └─┘  
par    └────────┘ └┘   └──┘    └──┘   └───┘         └─┘  
pid    └─────┘└─┘ └┘   └──┘    └──┘   └───┘         └─┘  
st   ─────────────────────────────────────────────────────────────┘└─
147    { /- For the (much easier) reverse inequality, we start from a point `x ∈ t0` and we want
st   ───┘└───────────────────────────────────────────────────────────────────────────────────────
148          to find a point `y ∈ s n` which is close to `x`.
st   ─────────────────────────────────────────────────────────
149          `x` belongs to `t0`, the intersection of the closures. In particular, it is well
st   ─────────────────────────────────────────────────────────────────────────────────────────
150          approximated by a point `z` in `⋃m≥n, s m`, say in `s m`. Since `s m` and
st   ──────────────────────────────────────────────────────────────────────────────────
151          `s n` are close, this point is itself well approximated by a point `y` in `s n`,
st   ─────────────────────────────────────────────────────────────────────────────────────────
152          as required. -/
st   ────────────────────────
153      assume n x xt0,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ─────────────────┘└─
154      have : x ∈ closure (⋃m≥n, (s m).val), by apply mem_Inter.1 xt0 n,
id                 └─────┘                         └───────┘   └─┘ 
src      └─────┘  └─────┘ └┘    └────┘     └────┘└───────┘└─┘   
typ      └─────┘ └─────┘ └┘  └────┘     └────┘└───────┘└─┘└─┘
doc      └─────┘  └─────┘ └┘    └────┘     └────┘         └─┘   
txt      └─────┘           └┘     └────┘     └────┘         └─┘   
par      └─────┘           └┘     └────┘     └────┘         └─┘   
pid      └───┘└┘           └┘     └────┘                   └─┘   
st   ───────────────────────────────────────┘                            └─
155      rcases mem_closure_iff'.1 this (B n) (B_pos n) with ⟨z, hz, Dxz⟩,
id              └──────────────┘   └──┘       └───┘ 
src      └─────┘└──────────────┘└─┘       └┘       └─────────────────┘
typ      └─────┘└──────────────┘└─┘└──┘  └┘ └───┘└─────────────────┘
doc      └─────┘└──────────────┘└─┘       └┘       └─────────────────┘
txt      └─────┘                └─┘       └┘       └─────────────────┘
par      └─────┘                └─┘       └┘       └─────────────────┘
pid                            └─┘       └┘       └─────────────────┘
st   ───────────────────────────────────────────────────────────────────┘└─
156      -- z : α,  Dxz : edist x z < B n,
st   ──────────────────────────────────────
157      simp only [exists_prop, set.mem_Union] at hz,
id                  └─────────┘  └───────────┘
src      └─────────┘└─────────┘└┘└───────────┘└─────┘
typ      └─────────┘└─────────┘└┘└───────────┘└─────┘
doc      └─────────┘           └┘             └─────┘
txt      └─────────┘           └┘             └─────┘
par      └─────────┘           └┘             └─────┘
pid          └──┘└┘           └┘             └───┘
st   ───────────────────────────────────────────────┘└─
158      rcases hz with ⟨m, ⟨m_ge_n, hm⟩⟩,
id              └┘
src      └─────┘  └─────────────────────┘
typ      └─────┘└┘└─────────────────────┘
doc      └─────┘  └─────────────────────┘
txt      └─────┘  └─────────────────────┘
par      └─────┘  └─────────────────────┘
pid              └─────────────────────┘
st   ───────────────────────────────────┘└─
159      -- m : ℕ, m_ge_n : m ≥ n, hm : z ∈ (s m).val
st   ─────────────────────────────────────────────────
160      have : Hausdorff_edist (s m).val (s n).val < B n := hs n m n m_ge_n (le_refl n),
id              └─────────────┘                          └┘      └────┘  └─────┘ 
src      └─────┘└─────────────┘   └────┘   └────┘   └──┘            └─────┘ 
typ      └─────┘└─────────────┘  └────┘  └────┘ └──┘└┘  └────┘ └─────┘
doc      └─────┘└─────────────┘   └────┘   └────┘   └──┘                    
txt      └─────┘                  └────┘   └────┘   └──┘                    
par      └─────┘                  └────┘   └────┘   └──┘                    
pid      └───┘└┘                  └────┘   └────┘   └──┘                    
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
161      rcases exists_edist_lt_of_Hausdorff_edist_lt hm this with ⟨y, hy, Dzy⟩,
id              └───────────────────────────────────┘ └┘ └──┘
src      └─────┘└───────────────────────────────────┘      └────────────────┘
typ      └─────┘└───────────────────────────────────┘└┘└──┘└────────────────┘
doc      └─────┘└───────────────────────────────────┘      └────────────────┘
txt      └─────┘                                           └────────────────┘
par      └─────┘                                           └────────────────┘
pid                                                       └────────────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
162      -- y : α,  hy : y ∈ (s n).val,  Dzy : edist z y < B n
st   ──────────────────────────────────────────────────────────
163      exact ⟨y, hy, calc
id                 └┘
src      └────┘  └┘  └┘    
typ      └────┘  └┘└┘└┘    
doc      └────┘  └┘  └┘    
txt      └────┘  └┘  └┘    
par      └────┘  └┘  └┘    
pid             └┘  └┘    
st   ───────────────────────
164        edist x y ≤ edist x z + edist z y : edist_triangle _ _ _
id                                └───┘     └────────────┘
src  ─────┘                └───┘  └─┘└────────────┘└──────
typ  ─────┘               └───┘└─┘└────────────┘└──────
doc  ─────┘                       └─┘              └──────
txt  ─────┘                       └─┘              └──────
par  ─────┘                       └─┘              └──────
pid  ─────┘                       └─┘              └──────
st   ───────────────────────────────────────────────────────────────
165              ... ≤ B n + B n : add_le_add' (le_of_lt Dxz) (le_of_lt Dzy)
id                                 └─────────┘           └─┘   └──────┘ └─┘
src  ───────────────┘      └─┘└─────────┘            └┘ └──────┘   └─
typ  ───────────────┘      └─┘└─────────┘         └─┘└┘ └──────┘└─┘└─
doc  ───────────────┘      └─┘                       └┘            └─
txt  ───────────────┘      └─┘                       └┘            └─
par  ───────────────┘      └─┘                       └┘            └─
pid  ───────────────┘      └─┘                       └┘            └─
st   ────────────────────────────────────────────────────────────────────────
166              ... = 2 * B n : (two_mul _).symm ⟩ },
id                              └─────┘
src  ───────────────┘ └─┘   └─┘ └─────┘└─────────┘
typ  ───────────────┘ └─┘ └─┘ └─────┘└─────────┘
doc  ───────────────┘ └─┘   └─┘        └─────────┘
txt  ───────────────┘ └─┘   └─┘        └─────────┘
par  ───────────────┘ └─┘   └─┘        └─────────┘
pid  ───────────────┘ └─┘   └─┘        └────────┘
st   ──────────────────────────────────────────────┘└┘
167    -- Deduce from the above inequalities that the distance between `s n` and `t0` is at most `2 B n`.
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
168    have main : ∀n:ℕ, edist (s n) t ≤ 2 * B n := λn, Hausdorff_edist_le_of_mem_edist (I1 n) (I2 n),
id                       └───┘                       └─────────────────────────────┘  └┘     └┘
src    └──────────┘ └┘  └───┘   └┘  └─┘   └──┘ └─┘└─────────────────────────────┘    └┘    
typ    └──────────┘ └┘  └───┘  └┘ └─┘  └──┘ └─┘└─────────────────────────────┘ └┘ └┘ └┘ 
doc    └──────────┘ └┘          └┘  └─┘   └──┘ └─┘└─────────────────────────────┘    └┘    
txt    └──────────┘ └┘          └┘  └─┘   └──┘ └─┘                                   └┘    
par    └──────────┘ └┘          └┘  └─┘   └──┘ └─┘                                   └┘    
pid    └───────┘└─┘ └┘          └┘  └─┘   └──┘ └─┘                                   └┘    
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
169    -- from this, the convergence of `s n` to `t0` follows.
st   ──────────────────────────────────────────────────────────
170    refine (tendsto_at_top _).2 (λε εpos, _),
id             └────────────┘
src    └─────┘ └────────────┘└────┘  └────────┘
typ    └─────┘ └────────────┘└────┘  └────────┘
doc    └─────┘               └────┘  └────────┘
txt    └─────┘               └────┘  └────────┘
par    └─────┘               └────┘  └────────┘
pid                         └────┘  └────────┘
st   ─────────────────────────────────────────┘└─
171    have : tendsto (λn, 2 * B n) at_top (𝓝 (2 * 0)),
id            └─────┘              └────┘  
src    └─────┘└─────┘  └───┘   └┘└────┘  └┘ └──┘
typ    └─────┘└─────┘  └───┘  └┘└────┘  └┘ └──┘
doc    └─────┘└─────┘  └───┘   └┘└────┘  └┘ └──┘
txt    └─────┘         └───┘   └┘         └┘ └──┘
par    └─────┘         └───┘   └┘         └┘ └──┘
pid    └───┘└┘         └───┘   └┘         └┘ └──┘
st   ────────────────────────────────────────────────┘└─
172      from ennreal.tendsto.const_mul
id            └───────────────────────┘
src      └───┘└───────────────────────┘
typ      └───┘└───────────────────────┘
doc      └───┘                         
txt      └───┘                         
par      └───┘                         
pid      └───┘                         
st   ───────────────────────────────────
173        (ennreal.tendsto_pow_at_top_nhds_0_of_lt_1 $ by simp [ennreal.one_lt_two])
id          └───────────────────────────────────────┘            └────────────────┘
src  ─────┘ └───────────────────────────────────────┘   └────┘└────────────────┘└─
typ  ─────┘ └───────────────────────────────────────┘   └────┘└────────────────┘└─
doc  ─────┘                                             └────┘                  └─
txt  ─────┘                                             └────┘                  └─
par  ─────┘                                             └────┘                  └─
pid  ─────┘                                             └─────┘                  └──
st   ────────────────────────────────────────────────────┘└────────────────────────┘└─
174        (or.inr $ by simp),
id          └────┘
src  ─────┘ └────┘   └──┘
typ  ─────┘ └────┘   └──┘
doc  ─────┘          └──┘
txt  ─────┘          └──┘
par  ─────┘          └──┘
pid  ─────┘          └────┘
st   ─────────────────┘└───┘└─
175    rw mul_zero at this,
id        └──────┘
src    └─┘└──────┘└──────┘
typ    └─┘└──────┘└──────┘
doc    └─┘        └──────┘
txt    └─┘        └──────┘
par    └─┘        └──────┘
pid              └──────┘
st   ────────────────────┘└─
176    obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b,
id                                        
src    └───────────────┘└┘ └───┘   └─┘  
typ    └───────────────┘└┘ └───┘  └─┘ 
doc    └───────────────┘ └┘  └───┘    └─┘  
txt    └───────────────┘ └┘  └───┘    └─┘  
par    └───────────────┘ └┘  └───┘    └─┘  
pid          └─────────┘ └┘  └───┘    └─┘  
st   ───────────────────────────────────────────┘└─
177      from ((tendsto_order.1 this).2 ε εpos).exists_forall_of_at_top,
id              └───────────┘   └──┘     └──┘
src      └───┘  └───────────┘└─┘    └──┘     └───────────────────────┘
typ      └───┘  └───────────┘└─┘└──┘└──┘└──┘└───────────────────────┘
doc      └───┘               └─┘    └──┘     └───────────────────────┘
txt      └───┘               └─┘    └──┘     └───────────────────────┘
par      └───┘               └─┘    └──┘     └───────────────────────┘
pid      └───┘               └─┘    └──┘     └──────────────────────┘
st   ─────────────────────────────────────────────────────────────────┘└─
178    exact ⟨N, λn hn, lt_of_le_of_lt (main n) (hN n hn)⟩
id                     └────────────┘  └──┘     └┘
src    └────┘  └┘ └────┘└────────────┘      └┘      └─┘
typ    └────┘ └┘ └────┘└────────────┘ └──┘ └┘ └┘   └─┘
doc    └────┘  └┘ └────┘                    └┘      └─┘
txt    └────┘  └┘ └────┘                    └┘      └─┘
par    └────┘  └┘ └────┘                    └┘      └─┘
pid           └┘ └────┘                    └┘      └┘
st   ─────────────────────────────────────────────────────┘
179  end
st   └─┘
180  
181  /-- In a compact space, the type of closed subsets is compact. -/
182  instance closeds.compact_space [compact_space α] : compact_space (closeds α) :=
id                                   └───────────┘     └───────────┘  └─────┘ 
src                                  └───────────┘      └───────────┘  └─────┘
typ                                  └───────────┘     └───────────┘  └─────┘ 
doc                                  └───────────┘      └───────────┘  └─────┘
183  ⟨begin
st    └─────
184    /- by completeness, it suffices to show that it is totally bounded,
st   ──────────────────────────────────────────────────────────────────────
185      i.e., for all ε>0, there is a finite set which is ε-dense.
st   ───────────────────────────────────────────────────────────────
186      start from a set `s` which is ε-dense in α. Then the subsets of `s`
st   ────────────────────────────────────────────────────────────────────────
187      are finitely many, and ε-dense for the Hausdorff distance. -/
st   ──────────────────────────────────────────────────────────────────
188    refine compact_of_totally_bounded_is_closed (emetric.totally_bounded_iff.2 (λε εpos, _)) is_closed_univ,
id            └──────────────────────────────────┘  └─────────────────────────┘                 └────────────┘
src    └─────┘└──────────────────────────────────┘ └─────────────────────────┘└─┘  └──────────┘└────────────┘
typ    └─────┘└──────────────────────────────────┘ └─────────────────────────┘└─┘  └──────────┘└────────────┘
doc    └─────┘                                                                └─┘  └──────────┘
txt    └─────┘                                                                └─┘  └──────────┘
par    └─────┘                                                                └─┘  └──────────┘
pid                                                                          └─┘  └──────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
189    rcases dense εpos with ⟨δ, δpos, δlt⟩,
id            └───┘ └──┘
src    └─────┘└───┘    └──────────────────┘
typ    └─────┘└───┘└──┘└──────────────────┘
doc    └─────┘         └──────────────────┘
txt    └─────┘         └──────────────────┘
par    └─────┘         └──────────────────┘
pid                   └──────────────────┘
st   ──────────────────────────────────────┘└─
190    rcases emetric.totally_bounded_iff.1 (compact_iff_totally_bounded_complete.1 (@compact_univ α _ _)).1 δ δpos
id            └─────────────────────────┘    └──────────────────────────────────┘     └──────────┘           └──┘
src    └─────┘└─────────────────────────┘└─┘ └──────────────────────────────────┘└─┘  └──────────┘ └───────┘     
typ    └─────┘└─────────────────────────┘└─┘ └──────────────────────────────────┘└─┘  └──────────┘└───────┘└──┘
doc    └─────┘                           └─┘                                     └─┘               └───────┘     
txt    └─────┘                           └─┘                                     └─┘               └───────┘     
par    └─────┘                           └─┘                                     └─┘               └───────┘     
pid                                     └─┘                                     └─┘               └───────┘     
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────
191      with ⟨s, fs, hs⟩,
src  ───────────────────┘
typ  ───────────────────┘
doc  ───────────────────┘
txt  ───────────────────┘
par  ───────────────────┘
pid  ───────────────────┘
st   ───────────────────┘└─
192    -- s : set α,  fs : finite s,  hs : univ ⊆ ⋃ (y : α) (H : y ∈ s), eball y δ
st   ──────────────────────────────────────────────────────────────────────────────
193    -- we first show that any set is well approximated by a subset of `s`.
st   ─────────────────────────────────────────────────────────────────────────
194    have main : ∀ u : set α, ∃v ⊆ s, Hausdorff_edist u v ≤ δ,
id                       └─┘        └─────────────┘      
src    └──────────┘ └───┘└─┘  └──┘ └─────────────┘  
typ    └──────────┘ └───┘└─┘ └──┘└─────────────┘  
doc    └──────────┘ └───┘      └──┘  └─────────────┘   
txt    └──────────┘ └───┘      └──┘                    
par    └──────────┘ └───┘      └──┘                    
pid    └───────┘└─┘ └───┘      └──┘                    
st   ─────────────────────────────────────────────────────────┘└─
195    { assume u,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
196      let v := {x : α | x ∈ s ∧ ∃y∈u, edist x y < δ},
id                                └───┘      
src      └───────┘└──┘ └─┘    └┘ └───┘   
typ      └───────┘└──┘└─┘  └┘└───┘  
doc      └───────┘ └──┘ └─┘     └┘           
txt      └───────┘ └──┘ └─┘     └┘           
par      └───────┘ └──┘ └─┘     └┘           
pid      └───┘└─┘ └──┘ └─┘     └┘           
st   ─────────────────────────────────────────────────┘└─
197      existsi [v, ((λx hx, hx.1) : v ⊆ s)],
id                                      
src      └───────┘ └┘   └────┘  └────┘   └┘
typ      └───────┘└┘   └────┘  └────┘ └┘
doc      └───────┘ └┘   └────┘  └────┘   └┘
txt      └───────┘ └┘   └────┘  └────┘   └┘
par      └───────┘ └┘   └────┘  └────┘   └┘
pid             └┘ └┘   └────┘  └────┘   └┘
st   ───────────────────────────────────────┘└─
198      refine Hausdorff_edist_le_of_mem_edist _ _,
id              └─────────────────────────────┘
src      └─────┘└─────────────────────────────┘└──┘
typ      └─────┘└─────────────────────────────┘└──┘
doc      └─────┘└─────────────────────────────┘└──┘
txt      └─────┘                               └──┘
par      └─────┘                               └──┘
pid                                           └──┘
st   ─────────────────────────────────────────────┘└─
199      { assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ─────┘└─────────┘└─
200        have : x ∈ ⋃y ∈ s, ball y δ := hs (by simp),
id                        └──┘       └┘
src        └─────┘  └──┘ └──┘  └──┘     └──┘
typ        └─────┘ └──┘└──┘ └──┘└┘   └──┘
doc        └─────┘  └──┘ └──┘  └──┘     └──┘
txt        └─────┘   └──┘        └──┘     └──┘
par        └─────┘   └──┘        └──┘     └──┘
pid        └───┘└┘   └──┘        └──┘     └────┘
st   ──────────────────────────────────────────┘└───┘└─
201        rcases mem_bUnion_iff.1 this with ⟨y, ys, dy⟩,
id                └────────────┘   └──┘
src        └─────┘└────────────┘└─┘    └───────────────┘
typ        └─────┘└────────────┘└─┘└──┘└───────────────┘
doc        └─────┘              └─┘    └───────────────┘
txt        └─────┘              └─┘    └───────────────┘
par        └─────┘              └─┘    └───────────────┘
pid                            └─┘    └───────────────┘
st   ──────────────────────────────────────────────────┘└─
202        have : edist y x < δ := by simp at dy; rwa [edist_comm] at dy,
id                └───┘                             └────────┘
src        └─────┘└───┘    └──┘  └────────┘└┘└───┘└────────┘└─────┘
typ        └─────┘└───┘ └──┘  └────────┘└┘└───┘└────────┘└─────┘
doc        └─────┘         └──┘  └────────┘└┘└───┘          └─────┘
txt        └─────┘         └──┘  └────────┘└┘└───┘          └─────┘
par        └─────┘         └──┘  └────────┘└┘└───┘          └─────┘
pid        └───┘└┘         └──┘  └────────────────┘          └─────┘
st   ───────────────────────────────┘└────────────────┘└────────┘└────┘└─
203        exact ⟨y, ⟨ys, ⟨x, hx, this⟩⟩, le_of_lt dy⟩ },
id                   └┘     └┘  └──┘    └──────┘ └┘
src        └────┘  └┘   └┘  └┘  └┘    └──┘└──────┘  └┘
typ        └────┘ └┘ └┘└┘ └┘└┘└┘└──┘└──┘└──────┘└┘└┘
doc        └────┘  └┘   └┘  └┘  └┘    └──┘          └┘
txt        └────┘  └┘   └┘  └┘  └┘    └──┘          └┘
par        └────┘  └┘   └┘  └┘  └┘    └──┘          └┘
pid               └┘   └┘  └┘  └┘    └──┘          
st   ─────────────────────────────────────────────────┘└┘
204      { rintros x ⟨hx1, ⟨y, yu, hy⟩⟩,
src        └──────────────────────────┘
typ        └──────────────────────────┘
doc        └──────────────────────────┘
txt        └──────────────────────────┘
par        └──────────────────────────┘
pid               └───────────────────┘
st   ─────────────────────────────────┘└─
205        exact ⟨y, yu, le_of_lt hy⟩ }},
id                  └┘  └──────┘ └┘
src        └────┘  └┘  └┘└──────┘  └┘
typ        └────┘ └┘└┘└┘└──────┘└┘└┘
doc        └────┘  └┘  └┘          └┘
txt        └────┘  └┘  └┘          └┘
par        └────┘  └┘  └┘          └┘
pid               └┘  └┘          
st   ────────────────────────────────┘└─┘
206    -- introduce the set F of all subsets of `s` (seen as members of `closeds α`).
st   ─────────────────────────────────────────────────────────────────────────────────
207    let F := {f : closeds α | f.val ⊆ s},
id                  └─────┘     └──┘   
src    └───────┘└──┘└─────┘ └─┘ └──┘  
typ    └───────┘└──┘└─────┘└─┘ └──┘ 
doc    └───────┘ └──┘└─────┘ └─┘       
txt    └───────┘ └──┘        └─┘       
par    └───────┘ └──┘        └─┘       
pid    └───┘└─┘ └──┘        └─┘       
st   ─────────────────────────────────────┘└─
208    use F,
id         
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
pid       
st   ──────┘└─
209    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
210    -- `F` is finite
st   ───────────────────
211    { apply @finite_of_finite_image _ _ F (λf, f.val),
id              └────────────────────┘     
src      └────┘ └────────────────────┘└───┘   └─┘     
typ      └────┘ └────────────────────┘└───┘  └─┘     
doc      └────┘                       └───┘   └─┘     
txt      └────┘                       └───┘   └─┘     
par      └────┘                       └───┘   └─┘     
pid                                  └───┘   └─┘     
st   ───┘└─────────────────────────────────────────────┘└─
212      { apply set.inj_on_of_injective, simp [subtype.val_injective] },
id               └─────────────────────┘        └───────────────────┘
src        └────┘└─────────────────────┘  └────┘└───────────────────┘└┘
typ        └────┘└─────────────────────┘  └────┘└───────────────────┘└┘
doc        └────┘                         └────┘                     └┘
txt        └────┘                         └────┘                     └┘
par        └────┘                         └────┘                     └┘
pid                                                               
st   ─────┘└───────────────────────────┘└─────────────────────────────┘└┘
213      { refine finite_subset (finite_subsets_of_finite fs) (λb, _),
id                └───────────┘  └──────────────────────┘ └┘
src        └─────┘└───────────┘ └──────────────────────┘  └┘  └───┘
typ        └─────┘└───────────┘ └──────────────────────┘└┘└┘  └───┘
doc        └─────┘              └──────────────────────┘  └┘  └───┘
txt        └─────┘                                        └┘  └───┘
par        └─────┘                                        └┘  └───┘
pid                                                      └┘  └───┘
st   ───────────────────────────────────────────────────────────────┘└─
214        simp only [and_imp, set.mem_image, set.mem_set_of_eq, exists_imp_distrib],
id                    └─────┘  └───────────┘  └───────────────┘  └────────────────┘
src        └─────────┘└─────┘└┘└───────────┘└┘└───────────────┘└┘└────────────────┘
typ        └─────────┘└─────┘└┘└───────────┘└┘└───────────────┘└┘└────────────────┘
doc        └─────────┘       └┘             └┘                 └┘                  
txt        └─────────┘       └┘             └┘                 └┘                  
par        └─────────┘       └┘             └┘                 └┘                  
pid            └──┘└┘       └┘             └┘                 └┘                  
st   ──────────────────────────────────────────────────────────────────────────────┘└─
215        assume x hx hx',
src        └─────────────┘
typ        └─────────────┘
doc        └─────────────┘
txt        └─────────────┘
par        └─────────────┘
pid        └─────────────┘
st   ────────────────────┘└─
216        rwa hx' at hx }},
id             └─┘
src        └──┘   └─────┘
typ        └──┘└─┘└─────┘
doc        └──┘   └─────┘
txt        └──┘   └─────┘
par        └──┘   └─────┘
pid              └────┘
st   ───────────────────┘└─┘
217    -- `F` is ε-dense
st   ────────────────────
218    { assume u _,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid      └────────┘
st   ─────────────┘└─
219      rcases main u.val with ⟨t0, t0s, Dut0⟩,
id              └──┘ └───┘
src      └─────┘    └───┘└───────────────────┘
typ      └─────┘└──┘└───┘└───────────────────┘
doc      └─────┘         └───────────────────┘
txt      └─────┘         └───────────────────┘
par      └─────┘         └───────────────────┘
pid                     └───────────────────┘
st   ─────────────────────────────────────────┘└─
220      have : is_closed t0 := closed_of_compact _ (finite_subset fs t0s).compact,
id              └───────┘ └┘    └───────────────┘    └───────────┘ └┘ └─┘
src      └─────┘└───────┘  └──┘└───────────────┘└─┘ └───────────┘     └───────┘
typ      └─────┘└───────┘└┘└──┘└───────────────┘└─┘ └───────────┘└┘└─┘└───────┘
doc      └─────┘└───────┘  └──┘                 └─┘                   └───────┘
txt      └─────┘           └──┘                 └─┘                   └───────┘
par      └─────┘           └──┘                 └─┘                   └───────┘
pid      └───┘└┘           └──┘                 └─┘                   └──────┘
st   ────────────────────────────────────────────────────────────────────────────┘└─
221      let t : closeds α := ⟨t0, this⟩,
id               └─────┘      └┘  └──┘
src      └──────┘└─────┘ └──┘   └┘    
typ      └──────┘└─────┘└──┘ └┘└┘└──┘
doc      └──────┘└─────┘ └──┘   └┘    
txt      └──────┘        └──┘   └┘    
par      └──────┘        └──┘   └┘    
pid      └───┘└─┘        └──┘   └┘    
st   ──────────────────────────────────┘└─
222      have : t ∈ F := t0s,
id                     └─┘
src      └─────┘   └──┘
typ      └─────┘ └──┘└─┘
doc      └─────┘   └──┘
txt      └─────┘   └──┘
par      └─────┘   └──┘
pid      └───┘└┘   └──┘
st   ──────────────────────┘└─
223      have : edist u t < ε := lt_of_le_of_lt Dut0 δlt,
id              └───┘         └────────────┘ └──┘ └─┘
src      └─────┘└───┘    └──┘└────────────┘    
typ      └─────┘└───┘ └──┘└────────────┘└──┘└─┘
doc      └─────┘         └──┘                  
txt      └─────┘         └──┘                  
par      └─────┘         └──┘                  
pid      └───┘└┘         └──┘                  
st   ──────────────────────────────────────────────────┘└─
224      apply mem_bUnion_iff.2,
id             └────────────┘
src      └────┘└────────────┘└┘
typ      └────┘└────────────┘└┘
doc      └────┘              └┘
txt      └────┘              └┘
par      └────┘              └┘
pid                         └┘
st   ─────────────────────────┘└─
225      exact ⟨t, ‹t ∈ F›, this⟩ }
id                      └──┘
src      └────┘  └┘   └┘    └┘
typ      └────┘  └┘ └┘└──┘└┘
doc      └────┘  └┘   └┘    └┘
txt      └────┘  └┘     └┘    └┘
par      └────┘  └┘     └┘    └┘
pid             └┘     └┘    
st   ────────────────────────────┘└─
226  end⟩
st   ──┘
227  
228  /-- In an emetric space, the type of non-empty compact subsets is an emetric space,
229  where the edistance is the Hausdorff edistance -/
230  instance nonempty_compacts.emetric_space : emetric_space (nonempty_compacts α) :=
id                                              └───────────┘  └───────────────┘ 
src                                             └───────────┘  └───────────────┘
typ                                             └───────────┘  └───────────────┘ 
doc                                             └───────────┘  └───────────────┘
231  { edist               := λs t, Hausdorff_edist s.val t.val,
id                               └─────────────┘ └──┘ └──┘
src                                └─────────────┘  └──┘  └──┘
typ                              └─────────────┘ └──┘ └──┘
doc                                 └─────────────┘
232    edist_self          := λs, Hausdorff_edist_self,
id                               └──────────────────┘
src                               └──────────────────┘
typ                              └──────────────────┘
doc                               └──────────────────┘
233    edist_comm          := λs t, Hausdorff_edist_comm,
id                                └──────────────────┘
src                                 └──────────────────┘
typ                               └──────────────────┘
doc                                 └──────────────────┘
234    edist_triangle      := λs t u, Hausdorff_edist_triangle,
id                                 └──────────────────────┘
src                                   └──────────────────────┘
typ                                └──────────────────────┘
doc                                   └──────────────────────┘
235    eq_of_edist_eq_zero := λs t h, subtype.eq $ begin
id                                 └────────┘
src                                   └────────┘
typ                                └────────┘
st                                                 └─────
236      have : closure (s.val) = closure (t.val) := Hausdorff_edist_zero_iff_closure_eq_closure.1 h,
id                       └───┘   └─────┘  └───┘     └─────────────────────────────────────────┘   
src      └─────┘        └───┘└┘└─────┘ └───┘└───┘└─────────────────────────────────────────┘└─┘
typ      └─────┘        └───┘└┘└─────┘ └───┘└───┘└─────────────────────────────────────────┘└─┘
doc      └─────┘             └┘ └─────┘      └───┘└─────────────────────────────────────────┘└─┘
txt      └─────┘             └┘              └───┘                                           └─┘
par      └─────┘             └┘              └───┘                                           └─┘
pid      └───┘└┘             └┘              └──┘                                           └─┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
237      rwa [closure_eq_iff_is_closed.2 (closed_of_compact _ s.property.2),
id            └──────────────────────┘    └───────────────┘   └────────┘
src      └───┘└──────────────────────┘└─┘ └───────────────┘└─┘└────────┘└────
typ      └───┘└──────────────────────┘└─┘ └───────────────┘└─┘└────────┘└────
doc      └───┘                        └─┘                  └─┘          └────
txt      └───┘                        └─┘                  └─┘          └────
par      └───┘                        └─┘                  └─┘          └────
pid         └┘                        └─┘                  └─┘          └────
st   ─────────────────────────────────────────────────────────────────────┘└─
238                closure_eq_iff_is_closed.2 (closed_of_compact _ t.property.2)] at this,
id                 └──────────────────────┘    └───────────────┘   └────────┘
src  ─────────────┘└──────────────────────┘└─┘ └───────────────┘└─┘└────────┘└──────────┘
typ  ─────────────┘└──────────────────────┘└─┘ └───────────────┘└─┘└────────┘└──────────┘
doc  ─────────────┘                        └─┘                  └─┘          └──────────┘
txt  ─────────────┘                        └─┘                  └─┘          └──────────┘
par  ─────────────┘                        └─┘                  └─┘          └──────────┘
pid  ─────────────┘                        └─┘                  └─┘          └──┘└──────┘
st   ──────────────────────────────────────────────────────────────────────────┘└──────┘└─
239    end }
st   ────┘
240  
241  /-- `nonempty_compacts.to_closeds` is a uniform embedding (as it is an isometry) -/
242  lemma nonempty_compacts.to_closeds.uniform_embedding :
243    uniform_embedding (@nonempty_compacts.to_closeds α _ _) :=
id     └───────────────┘   └──────────────────────────┘ 
src    └───────────────┘   └──────────────────────────┘
typ    └───────────────┘   └──────────────────────────┘ 
doc                        └──────────────────────────┘
244  isometry.uniform_embedding $ λx y, rfl
id   └────────────────────────┘       └─┘
src  └────────────────────────┘         └─┘
typ  └────────────────────────┘       └─┘
doc  └────────────────────────┘
245  
246  /-- The range of `nonempty_compacts.to_closeds` is closed in a complete space -/
247  lemma nonempty_compacts.is_closed_in_closeds [complete_space α] :
id                                                 └────────────┘ 
src                                                └────────────┘
typ                                                └────────────┘ 
doc                                                └────────────┘
248    is_closed (nonempty_compacts.to_closeds '' (univ : set (nonempty_compacts α))) :=
id     └───────┘  └──────────────────────────┘ └┘  └──┘   └─┘  └───────────────┘ 
src    └───────┘  └──────────────────────────┘ └┘  └──┘   └─┘  └───────────────┘
typ    └───────┘  └──────────────────────────┘ └┘  └──┘   └─┘  └───────────────┘ 
doc    └───────┘  └──────────────────────────┘                 └───────────────┘
249  begin
st   └─────
250    have : nonempty_compacts.to_closeds '' univ = {s : closeds α | s.val.nonempty ∧ compact s.val},
id            └──────────────────────────┘ └┘ └──┘      └─────┘     └──┘└───────┘  └─────┘
src    └─────┘└──────────────────────────┘└┘└──┘└──┘└─────┘ └─┘ └──┘└───────┘└─────┘     
typ    └─────┘└──────────────────────────┘└┘└──┘└──┘└─────┘└─┘ └──┘└───────┘└─────┘     
doc    └─────┘└──────────────────────────┘        └──┘└─────┘ └─┘     └───────┘ └─────┘     
txt    └─────┘                                    └──┘        └─┘                           
par    └─────┘                                    └──┘        └─┘                           
pid    └───┘└┘                                    └──┘        └─┘                           
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
251    { ext,
src      └─┘
typ      └─┘
doc      └─┘
txt      └─┘
par      └─┘
st   ───┘└─┘└─
252      simp only [set.image_univ, set.mem_range, ne.def, set.mem_set_of_eq],
id                  └────────────┘  └───────────┘  └────┘  └───────────────┘
src      └─────────┘└────────────┘└┘└───────────┘└┘└────┘└┘└───────────────┘
typ      └─────────┘└────────────┘└┘└───────────┘└┘└────┘└┘└───────────────┘
doc      └─────────┘              └┘             └┘      └┘                 
txt      └─────────┘              └┘             └┘      └┘                 
par      └─────────┘              └┘             └┘      └┘                 
pid          └──┘└┘              └┘             └┘      └┘                 
st   ───────────────────────────────────────────────────────────────────────┘└─
253      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
254      { rintros ⟨y, hy⟩,
src        └─────────────┘
typ        └─────────────┘
doc        └─────────────┘
txt        └─────────────┘
par        └─────────────┘
pid               └──────┘
st   ─────┘└─────────────┘└─
255        have : x.val = y.val := by rcases hy; simp,
id                └───┘   └───┘              └┘
src        └─────┘└───┘ └───┘└──┘  └─────┘  └┘└──┘
typ        └─────┘└───┘ └───┘└──┘  └─────┘└┘└┘└──┘
doc        └─────┘           └──┘  └─────┘  └┘└──┘
txt        └─────┘           └──┘  └─────┘  └┘└──┘
par        └─────┘           └──┘  └─────┘  └┘└──┘
pid        └───┘└┘           └──┘  └──────┘  └────┘
st   ───────────────────────────────┘└──────────────┘└─
256        rw this,
id            └──┘
src        └─┘
typ        └─┘└──┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ────────────┘└─
257        exact y.property },
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘          
txt        └────┘          
par        └────┘          
pid                       
st   ──────────────────────┘└┘
258      { rintros ⟨hx1, hx2⟩,
src        └────────────────┘
typ        └────────────────┘
doc        └────────────────┘
txt        └────────────────┘
par        └────────────────┘
pid               └─────────┘
st   ───────────────────────┘└─
259        existsi (⟨x.val, ⟨hx1, hx2⟩⟩ : nonempty_compacts α),
id                   └───┘   └─┘  └─┘     └───────────────┘ 
src        └──────┘  └───┘└┘    └┘   └───┘└───────────────┘ 
typ        └──────┘  └───┘└┘ └─┘└┘└─┘└───┘└───────────────┘
doc        └──────┘       └┘    └┘   └───┘└───────────────┘ 
txt        └──────┘       └┘    └┘   └───┘                  
par        └──────┘       └┘    └┘   └───┘                  
pid                      └┘    └┘   └───┘                  
st   ────────────────────────────────────────────────────────┘└─
260        apply subtype.eq,
id               └────────┘
src        └────┘└────────┘
typ        └────┘└────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────────────┘└─
261        refl }},
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└─┘
262    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
263    refine is_closed_of_closure_subset (λs hs, _),
id            └─────────────────────────┘
src    └─────┘└─────────────────────────┘  └──────┘
typ    └─────┘└─────────────────────────┘  └──────┘
doc    └─────┘                             └──────┘
txt    └─────┘                             └──────┘
par    └─────┘                             └──────┘
pid                                       └──────┘
st   ──────────────────────────────────────────────┘└─
264    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
265    { -- take a set set t which is nonempty and at distance at most 1 of s
st   ───┘└────────────────────────────────────────────────────────────────────
266      rcases mem_closure_iff'.1 hs 1 ennreal.zero_lt_one with ⟨t, ht, Dst⟩,
id              └──────────────┘   └┘   └─────────────────┘
src      └─────┘└──────────────┘└─┘  └─┘└─────────────────┘└────────────────┘
typ      └─────┘└──────────────┘└─┘└┘└─┘└─────────────────┘└────────────────┘
doc      └─────┘└──────────────┘└─┘  └─┘                   └────────────────┘
txt      └─────┘                └─┘  └─┘                   └────────────────┘
par      └─────┘                └─┘  └─┘                   └────────────────┘
pid                            └─┘  └─┘                   └────────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
267      rw edist_comm at Dst,
id          └────────┘
src      └─┘└────────┘└─────┘
typ      └─┘└────────┘└─────┘
doc      └─┘          └─────┘
txt      └─┘          └─────┘
par      └─┘          └─────┘
pid                  └─────┘
st   ───────────────────────┘└─
268      -- this set t contains a point x
st   ─────────────────────────────────────
269      rcases ht.1 with ⟨x, hx⟩,
id              └┘
src      └─────┘  └─────────────┘
typ      └─────┘└┘└─────────────┘
doc      └─────┘  └─────────────┘
txt      └─────┘  └─────────────┘
par      └─────┘  └─────────────┘
pid              └─────────────┘
st   ───────────────────────────┘└─
270      -- by the Hausdorff distance control, this point x is at distance at most 1
st   ────────────────────────────────────────────────────────────────────────────────
271      -- of a point y in s
st   ─────────────────────────
272      rcases exists_edist_lt_of_Hausdorff_edist_lt hx Dst with ⟨y, hy, _⟩,
id              └───────────────────────────────────┘ └┘ └─┘
src      └─────┘└───────────────────────────────────┘     └──────────────┘
typ      └─────┘└───────────────────────────────────┘└┘└─┘└──────────────┘
doc      └─────┘└───────────────────────────────────┘     └──────────────┘
txt      └─────┘                                          └──────────────┘
par      └─────┘                                          └──────────────┘
pid                                                      └──────────────┘
st   ──────────────────────────────────────────────────────────────────────┘└─
273      -- this shows that s is not empty
st   ──────────────────────────────────────
274      exact ⟨_, hy⟩ },
id                 └┘
src      └────┘ └─┘  └┘
typ      └────┘ └─┘└┘└┘
doc      └────┘ └─┘  └┘
txt      └────┘ └─┘  └┘
par      └────┘ └─┘  └┘
pid            └─┘  
st   ─────────────────┘└┘
275    { refine compact_iff_totally_bounded_complete.2 ⟨_, is_complete_of_is_closed s.property⟩,
id              └──────────────────────────────────┘       └──────────────────────┘ └────────┘
src      └─────┘└──────────────────────────────────┘└─┘ └─┘└──────────────────────┘└────────┘
typ      └─────┘└──────────────────────────────────┘└─┘ └─┘└──────────────────────┘└────────┘
doc      └─────┘                                    └─┘ └─┘                                  
txt      └─────┘                                    └─┘ └─┘                                  
par      └─────┘                                    └─┘ └─┘                                  
pid                                                └─┘ └─┘                                  
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
276      refine totally_bounded_iff.2 (λε εpos, _),
id              └─────────────────┘
src      └─────┘└─────────────────┘└─┘  └────────┘
typ      └─────┘└─────────────────┘└─┘  └────────┘
doc      └─────┘                   └─┘  └────────┘
txt      └─────┘                   └─┘  └────────┘
par      └─────┘                   └─┘  └────────┘
pid                               └─┘  └────────┘
st   ────────────────────────────────────────────┘└─
277      -- we have to show that s is covered by finitely many eballs of radius ε
st   ─────────────────────────────────────────────────────────────────────────────
278      -- pick a nonempty compact set t at distance at most ε/2 of s
st   ──────────────────────────────────────────────────────────────────
279      rcases mem_closure_iff'.1 hs (ε/2) (ennreal.half_pos εpos) with ⟨t, ht, Dst⟩,
id              └──────────────┘   └┘      └──────────────┘ └──┘
src      └─────┘└──────────────┘└─┘    └─┘ └──────────────┘    └─────────────────┘
typ      └─────┘└──────────────┘└─┘└┘ └─┘ └──────────────┘└──┘└─────────────────┘
doc      └─────┘└──────────────┘└─┘     └─┘                     └─────────────────┘
txt      └─────┘                └─┘     └─┘                     └─────────────────┘
par      └─────┘                └─┘     └─┘                     └─────────────────┘
pid                            └─┘     └─┘                     └─────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
280      -- cover this space with finitely many balls of radius ε/2
st   ───────────────────────────────────────────────────────────────
281      rcases totally_bounded_iff.1 (compact_iff_totally_bounded_complete.1 ht.2).1 (ε/2) (ennreal.half_pos εpos)
id              └─────────────────┘    └──────────────────────────────────┘   └┘            └──────────────┘ └──┘
src      └─────┘└─────────────────┘└─┘ └──────────────────────────────────┘└─┘  └────┘   └─┘ └──────────────┘    └─
typ      └─────┘└─────────────────┘└─┘ └──────────────────────────────────┘└─┘└┘└────┘  └─┘ └──────────────┘└──┘└─
doc      └─────┘                   └─┘                                     └─┘  └────┘   └─┘                     └─
txt      └─────┘                   └─┘                                     └─┘  └────┘   └─┘                     └─
par      └─────┘                   └─┘                                     └─┘  └────┘   └─┘                     └─
pid                               └─┘                                     └─┘  └────┘   └─┘                     └─
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────
282        with ⟨u, fu, ut⟩,
src  ─────────────────────┘
typ  ─────────────────────┘
doc  ─────────────────────┘
txt  ─────────────────────┘
par  ─────────────────────┘
pid  ─────────────────────┘
st   ─────────────────────┘└─
283      refine ⟨u, ⟨fu, λx hx, _⟩⟩,
id                  └┘
src      └─────┘  └┘   └┘ └───────┘
typ      └─────┘ └┘ └┘└┘ └───────┘
doc      └─────┘  └┘   └┘ └───────┘
txt      └─────┘  └┘   └┘ └───────┘
par      └─────┘  └┘   └┘ └───────┘
pid              └┘   └┘ └───────┘
st   ─────────────────────────────┘└─
284      -- u : set α,  fu : finite u,  ut : t.val ⊆ ⋃ (y : α) (H : y ∈ u), eball y (ε / 2)
st   ───────────────────────────────────────────────────────────────────────────────────────
285      -- then s is covered by the union of the balls centered at u of radius ε
st   ─────────────────────────────────────────────────────────────────────────────
286      rcases exists_edist_lt_of_Hausdorff_edist_lt hx Dst with ⟨z, hz, Dxz⟩,
id              └───────────────────────────────────┘ └┘ └─┘
src      └─────┘└───────────────────────────────────┘     └────────────────┘
typ      └─────┘└───────────────────────────────────┘└┘└─┘└────────────────┘
doc      └─────┘└───────────────────────────────────┘     └────────────────┘
txt      └─────┘                                          └────────────────┘
par      └─────┘                                          └────────────────┘
pid                                                      └────────────────┘
st   ────────────────────────────────────────────────────────────────────────┘└─
287      rcases mem_bUnion_iff.1 (ut hz) with ⟨y, hy, Dzy⟩,
id              └────────────┘    └┘ └┘
src      └─────┘└────────────┘└─┘     └─────────────────┘
typ      └─────┘└────────────┘└─┘ └┘└┘└─────────────────┘
doc      └─────┘              └─┘     └─────────────────┘
txt      └─────┘              └─┘     └─────────────────┘
par      └─────┘              └─┘     └─────────────────┘
pid                          └─┘     └─────────────────┘
st   ────────────────────────────────────────────────────┘└─
288      have : edist x y < ε := calc
id              └───┘    
src      └─────┘└───┘   └──┘    
typ      └─────┘└───┘└──┘    
doc      └─────┘         └──┘    
txt      └─────┘         └──┘    
par      └─────┘         └──┘    
pid      └───┘└┘         └──┘    
st   ─────────────────────────────────
289        edist x y ≤ edist x z + edist z y : edist_triangle _ _ _
id                                └───┘     └────────────┘
src  ─────┘                └───┘  └─┘└────────────┘└──────
typ  ─────┘               └───┘└─┘└────────────┘└──────
doc  ─────┘                       └─┘              └──────
txt  ─────┘                       └─┘              └──────
par  ─────┘                       └─┘              └──────
pid  ─────┘                       └─┘              └──────
st   ───────────────────────────────────────────────────────────────
290        ... < ε/2 + ε/2 : ennreal.add_lt_add Dxz Dzy
id                          └────────────────┘ └─┘ └─┘
src  ─────────┘   └┘  └──┘└────────────────┘      
typ  ─────────┘   └┘  └──┘└────────────────┘└─┘└─┘
doc  ─────────┘   └┘   └──┘                        
txt  ─────────┘   └┘   └──┘                        
par  ─────────┘   └┘   └──┘                        
pid  ─────────┘   └┘   └──┘                        
st   ───────────────────────────────────────────────────
291        ... = ε : ennreal.add_halves _,
id                  └────────────────┘
src  ─────────┘  └─┘└────────────────┘└┘
typ  ─────────┘ └─┘└────────────────┘└┘
doc  ─────────┘  └─┘                  └┘
txt  ─────────┘  └─┘                  └┘
par  ─────────┘  └─┘                  └┘
pid  ─────────┘  └─┘                  └┘
st   ───────────────────────────────────┘└─
292      exact mem_bUnion hy this },
id             └────────┘ └┘ └──┘
src      └────┘└────────┘      
typ      └────┘└────────┘└┘└──┘
doc      └────┘                
txt      └────┘                
par      └────┘                
pid                           
st   ────────────────────────────┘└──
293  end
st   ──┘
294  
295  /-- In a complete space, the type of nonempty compact subsets is complete. This follows
296  from the same statement for closed subsets -/
297  instance nonempty_compacts.complete_space [complete_space α] : complete_space (nonempty_compacts α) :=
id                                              └────────────┘     └────────────┘  └───────────────┘ 
src                                             └────────────┘      └────────────┘  └───────────────┘
typ                                             └────────────┘     └────────────┘  └───────────────┘ 
doc                                             └────────────┘      └────────────┘  └───────────────┘
298  begin
st   └─────
299    apply complete_space_of_is_complete_univ,
id           └────────────────────────────────┘
src    └────┘└────────────────────────────────┘
typ    └────┘└────────────────────────────────┘
doc    └────┘└────────────────────────────────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────────────────────┘└─
300    apply (is_complete_image_iff nonempty_compacts.to_closeds.uniform_embedding).1,
id            └───────────────────┘ └────────────────────────────────────────────┘
src    └────┘ └───────────────────┘└────────────────────────────────────────────┘└─┘
typ    └────┘ └───────────────────┘└────────────────────────────────────────────┘└─┘
doc    └────┘ └───────────────────┘└────────────────────────────────────────────┘└─┘
txt    └────┘                                                                    └─┘
par    └────┘                                                                    └─┘
pid                                                                             └┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
301    apply is_complete_of_is_closed,
id           └──────────────────────┘
src    └────┘└──────────────────────┘
typ    └────┘└──────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────────────┘└─
302    exact nonempty_compacts.is_closed_in_closeds
id           └────────────────────────────────────┘
src    └────┘└────────────────────────────────────┘
typ    └────┘└────────────────────────────────────┘
doc    └────┘└────────────────────────────────────┘
txt    └────┘                                      
par    └────┘                                      
pid                                               
st   ──────────────────────────────────────────────┘
303  end
st   └─┘
304  
305  /-- In a compact space, the type of nonempty compact subsets is compact. This follows from
306  the same statement for closed subsets -/
307  instance nonempty_compacts.compact_space [compact_space α] : compact_space (nonempty_compacts α) :=
id                                             └───────────┘     └───────────┘  └───────────────┘ 
src                                            └───────────┘      └───────────┘  └───────────────┘
typ                                            └───────────┘     └───────────┘  └───────────────┘ 
doc                                            └───────────┘      └───────────┘  └───────────────┘
308  ⟨begin
st    └─────
309    rw embedding.compact_iff_compact_image nonempty_compacts.to_closeds.uniform_embedding.embedding,
id        └─────────────────────────────────┘ └──────────────────────────────────────────────────────┘
src    └─┘└─────────────────────────────────┘└──────────────────────────────────────────────────────┘
typ    └─┘└─────────────────────────────────┘└──────────────────────────────────────────────────────┘
doc    └─┘                                   └──────────────────────────────────────────────────────┘
txt    └─┘                                   
par    └─┘                                   
pid                                         
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
310    exact nonempty_compacts.is_closed_in_closeds.compact
id           └────────────────────────────────────────────┘
src    └────┘└────────────────────────────────────────────┘
typ    └────┘└────────────────────────────────────────────┘
doc    └────┘└────────────────────────────────────────────┘
txt    └────┘                                              
par    └────┘                                              
pid                                                       
st   ──────────────────────────────────────────────────────┘
311  end⟩
st   └─┘
312  
313  /-- In a second countable space, the type of nonempty compact subsets is second countable -/
314  instance nonempty_compacts.second_countable_topology [second_countable_topology α] :
id                                                         └───────────────────────┘ 
src                                                        └───────────────────────┘
typ                                                        └───────────────────────┘ 
doc                                                        └───────────────────────┘
315    second_countable_topology (nonempty_compacts α) :=
id     └───────────────────────┘  └───────────────┘ 
src    └───────────────────────┘  └───────────────┘
typ    └───────────────────────┘  └───────────────┘ 
doc    └───────────────────────┘  └───────────────┘
316  begin
st   └─────
317    haveI : separable_space (nonempty_compacts α) :=
id             └─────────────┘  └───────────────┘ 
src    └──────┘└─────────────┘ └───────────────┘ └────
typ    └──────┘└─────────────┘ └───────────────┘└────
doc    └──────┘└─────────────┘ └───────────────┘ └────
txt    └──────┘                                  └────
par    └──────┘                                  └────
pid         └┘                                  └───
st   ───────────────────────────────────────────────────
318    begin
src  ─┘     
typ  ─┘     
doc  ─┘     
txt  ─┘     
par  ─┘     
pid  ─┘     
st   ─┘└─────
319      /- To obtain a countable dense subset of `nonempty_compacts α`, start from
src  ───────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────
320      a countable dense subset `s` of α, and then consider all its finite nonempty subsets.
src  ──────────────────────────────────────────────────────────────────────────────────────────
typ  ──────────────────────────────────────────────────────────────────────────────────────────
doc  ──────────────────────────────────────────────────────────────────────────────────────────
txt  ──────────────────────────────────────────────────────────────────────────────────────────
par  ──────────────────────────────────────────────────────────────────────────────────────────
pid  ──────────────────────────────────────────────────────────────────────────────────────────
st   ──────────────────────────────────────────────────────────────────────────────────────────
321      This set is countable and made of nonempty compact sets. It turns out to be dense:
src  ───────────────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────────────
322      by total boundedness, any compact set `t` can be covered by finitely many small balls, and
src  ───────────────────────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────────────────────
323      approximations in `s` of the centers of these balls give the required finite approximation
src  ───────────────────────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────────────────────
324      of `t`. -/
src  ───────────────
typ  ───────────────
doc  ───────────────
txt  ───────────────
par  ───────────────
pid  ───────────────
st   ───────────────
325      have : separable_space α := by apply_instance,
id              └─────────────┘ 
src  ───┘└─────┘└─────────────┘ └──┘  └────────────┘└─
typ  ───┘└─────┘└─────────────┘└──┘  └────────────┘└─
doc  ───┘└─────┘└─────────────┘ └──┘  └────────────┘└─
txt  ───┘└─────┘                └──┘  └────────────┘└─
par  ───┘└─────┘                └──┘  └────────────┘└─
pid  ──────────┘                └──┘  └────────────────
st   ─────────────────────────────────┘└─────────────┘└─
326      rcases this.exists_countable_closure_eq_univ with ⟨s, cs, s_dense⟩,
id              └───────────────────────────────────┘
src  ───┘└─────┘└───────────────────────────────────┘└────────────────────┘└─
typ  ───┘└─────┘└───────────────────────────────────┘└────────────────────┘└─
doc  ───┘└─────┘                                     └────────────────────┘└─
txt  ───┘└─────┘                                     └────────────────────┘└─
par  ───┘└─────┘                                     └────────────────────┘└─
pid  ──────────┘                                     └───────────────────────
st   ─────────────────────────────────────────────────────────────────────┘└─
327      let v0 := {t : set α | finite t ∧ t ⊆ s},
id                     └─┘    └────┘        
src  ───┘└────────┘└──┘└─┘ └─┘└────┘    └─
typ  ───┘└────────┘└──┘└─┘└─┘└────┘   └─
doc  ───┘└────────┘ └──┘    └─┘└────┘     └─
txt  ───┘└────────┘ └──┘    └─┘           └─
par  ───┘└────────┘ └──┘    └─┘           └─
pid  ─────────────┘ └──┘    └─┘           └──
st   ───────────────────────────────────────────┘└─
328      let v : set (nonempty_compacts α) := {t : nonempty_compacts α | t.val ∈ v0},
id               └─┘  └───────────────┘           └───────────────┘     └──┘  └┘
src  ───┘└──────┘└─┘ └───────────────┘ └───┘ └──┘└───────────────┘ └─┘ └──┘  └─
typ  ───┘└──────┘└─┘ └───────────────┘└───┘ └──┘└───────────────┘└─┘ └──┘└┘└─
doc  ───┘└──────┘    └───────────────┘ └───┘ └──┘└───────────────┘ └─┘        └─
txt  ───┘└──────┘                      └───┘ └──┘                  └─┘        └─
par  ───┘└──────┘                      └───┘ └──┘                  └─┘        └─
pid  ───────────┘                      └───┘ └──┘                  └─┘        └──
st   ──────────────────────────────────────────────────────────────────────────────┘└─
329      refine  ⟨⟨v, ⟨_, _⟩⟩⟩,
id                 
src  ───┘└──────┘   └┘ └─────┘└─
typ  ───┘└──────┘  └┘ └─────┘└─
doc  ───┘└──────┘   └┘ └─────┘└─
txt  ───┘└──────┘   └┘ └─────┘└─
par  ───┘└──────┘   └┘ └─────┘└─
pid  ───────────┘   └┘ └────────
st   ────────────────────────┘└─
330      { have : countable (subtype.val '' v),
id                └───────┘  └─────────┘ └┘ 
src  ─────┘└─────┘└───────┘ └─────────┘└┘ └─
typ  ─────┘└─────┘└───────┘ └─────────┘└┘└─
doc  ─────┘└─────┘└───────┘               └─
txt  ─────┘└─────┘                        └─
par  ─────┘└─────┘                        └─
pid  ────────────┘                        └──
st   ────┘└──────────────────────────────────┘└─
331        { refine countable_subset (λx hx, _) (countable_set_of_finite_subset cs),
id                  └──────────────┘             └────────────────────────────┘ └┘
src  ───────┘└─────┘└──────────────┘  └───────┘ └────────────────────────────┘  └─
typ  ───────┘└─────┘└──────────────┘  └───────┘ └────────────────────────────┘└┘└─
doc  ───────┘└─────┘                  └───────┘                                 └─
txt  ───────┘└─────┘                  └───────┘                                 └─
par  ───────┘└─────┘                  └───────┘                                 └─
pid  ──────────────┘                  └───────┘                                 └──
st   ──────┘└─────────────────────────────────────────────────────────────────────┘└─
332          rcases (mem_image _ _ _).1 hx with ⟨y, ⟨hy, yx⟩⟩,
id                   └───────┘          └┘
src  ───────┘└─────┘ └───────┘└────────┘  └─────────────────┘└─
typ  ───────┘└─────┘ └───────┘└────────┘└┘└─────────────────┘└─
doc  ───────┘└─────┘          └────────┘  └─────────────────┘└─
txt  ───────┘└─────┘          └────────┘  └─────────────────┘└─
par  ───────┘└─────┘          └────────┘  └─────────────────┘└─
pid  ──────────────┘          └────────┘  └────────────────────
st   ───────────────────────────────────────────────────────┘└─
333          rw ← yx,
id                └┘
src  ───────┘└───┘  └─
typ  ───────┘└───┘└┘└─
doc  ───────┘└───┘  └─
txt  ───────┘└───┘  └─
par  ───────┘└───┘  └─
pid  ────────────┘  └─
st   ──────────────┘└─
334          exact hy },
id                 └┘
src  ───────┘└────┘  └──
typ  ───────┘└────┘└┘└──
doc  ───────┘└────┘  └──
txt  ───────┘└────┘  └──
par  ───────┘└────┘  └──
pid  ─────────────┘  └───
st   ────────────────┘└─
335        apply countable_of_injective_of_countable_image _ this,
id               └───────────────────────────────────────┘   └──┘
src  ─────┘└────┘└───────────────────────────────────────┘└─┘    └─
typ  ─────┘└────┘└───────────────────────────────────────┘└─┘└──┘└─
doc  ─────┘└────┘                                         └─┘    └─
txt  ─────┘└────┘                                         └─┘    └─
par  ─────┘└────┘                                         └─┘    └─
pid  ───────────┘                                         └─┘    └─
st   ───────────────────────────────────────────────────────────┘└─
336        apply inj_on_of_inj_on_of_subset (injective_iff_inj_on_univ.1 subtype.val_injective)
id               └────────────────────────┘  └───────────────────────┘   └───────────────────┘
src  ─────┘└────┘└────────────────────────┘ └───────────────────────┘└─┘└───────────────────┘└─
typ  ─────┘└────┘└────────────────────────┘ └───────────────────────┘└─┘└───────────────────┘└─
doc  ─────┘└────┘                                                    └─┘                     └─
txt  ─────┘└────┘                                                    └─┘                     └─
par  ─────┘└────┘                                                    └─┘                     └─
pid  ───────────┘                                                    └─┘                     └─
st   ───────────────────────────────────────────────────────────────────────────────────────────
337          (subset_univ _) },
id            └─────────┘
src  ───────┘ └─────────┘└──┘└──
typ  ───────┘ └─────────┘└──┘└──
doc  ───────┘            └──┘└──
txt  ───────┘            └──┘└──
par  ───────┘            └──┘└──
pid  ───────┘            └──────
st   ───────────────────────┘└─
338      { refine subset.antisymm (subset_univ _) (λt ht, mem_closure_iff'.2 (λε εpos, _)),
id                └─────────────┘  └─────────┘            └──────────────┘
src  ─────┘└─────┘└─────────────┘ └─────────┘└──┘  └────┘└──────────────┘└─┘  └─────────┘└─
typ  ─────┘└─────┘└─────────────┘ └─────────┘└──┘  └────┘└──────────────┘└─┘  └─────────┘└─
doc  ─────┘└─────┘                           └──┘  └────┘└──────────────┘└─┘  └─────────┘└─
txt  ─────┘└─────┘                           └──┘  └────┘                └─┘  └─────────┘└─
par  ─────┘└─────┘                           └──┘  └────┘                └─┘  └─────────┘└─
pid  ────────────┘                           └──┘  └────┘                └─┘  └────────────
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
339        -- t is a compact nonempty set, that we have to approximate uniformly by a a set in `v`.
src  ───────────────────────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────────────────────
340        rcases dense εpos with ⟨δ, δpos, δlt⟩,
id                └───┘ └──┘
src  ─────┘└─────┘└───┘    └──────────────────┘└─
typ  ─────┘└─────┘└───┘└──┘└──────────────────┘└─
doc  ─────┘└─────┘         └──────────────────┘└─
txt  ─────┘└─────┘         └──────────────────┘└─
par  ─────┘└─────┘         └──────────────────┘└─
pid  ────────────┘         └─────────────────────
st   ──────────────────────────────────────────┘└─
341        -- construct a map F associating to a point in α an approximating point in s, up to δ/2.
src  ───────────────────────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────────────────────
342        have Exy : ∀x, ∃y, y ∈ s ∧ edist x y < δ/2,
id                                 └───┘      
src  ─────┘└─────────┘      └───┘   └─
typ  ─────┘└─────────┘     └───┘  └─
doc  ─────┘└─────────┘                  └─
txt  ─────┘└─────────┘                  └─
par  ─────┘└─────────┘                  └─
pid  ────────────────┘                  └──
st   ───────────────────────────────────────────────┘└─
343        { assume x,
src  ───────┘└──────┘└─
typ  ───────┘└──────┘└─
doc  ───────┘└──────┘└─
txt  ───────┘└──────┘└─
par  ───────┘└──────┘└─
pid  ──────────────────
st   ──────┘└───────┘└─
344          have : x ∈ closure s := by rw s_dense; exact mem_univ _,
id                     └─────┘           └─────┘        └──────┘
src  ───────┘└─────┘  └─────┘ └──┘  └─┘       └┘└────┘└──────┘└┘└─
typ  ───────┘└─────┘ └─────┘└──┘  └─┘└─────┘└┘└────┘└──────┘└┘└─
doc  ───────┘└─────┘  └─────┘ └──┘  └─┘       └┘└────┘        └┘└─
txt  ───────┘└─────┘          └──┘  └─┘       └┘└────┘        └┘└─
par  ───────┘└─────┘          └──┘  └─┘       └┘└────┘        └┘└─
pid  ──────────────┘          └──┘  └──┘       └──────┘        └───
st   ─────────────────────────────────┘└───────────────────────────┘└─
345          rcases mem_closure_iff'.1 this (δ/2) (ennreal.half_pos δpos) with ⟨y, ys, hy⟩,
id                  └──────────────┘   └──┘       └──────────────┘ └──┘
src  ───────┘└─────┘└──────────────┘└─┘       └─┘ └──────────────┘    └────────────────┘└─
typ  ───────┘└─────┘└──────────────┘└─┘└──┘  └─┘ └──────────────┘└──┘└────────────────┘└─
doc  ───────┘└─────┘└──────────────┘└─┘       └─┘                     └────────────────┘└─
txt  ───────┘└─────┘                └─┘       └─┘                     └────────────────┘└─
par  ───────┘└─────┘                └─┘       └─┘                     └────────────────┘└─
pid  ──────────────┘                └─┘       └─┘                     └───────────────────
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
346          exact ⟨y, ⟨ys, hy⟩⟩ },
id                     └┘  └┘
src  ───────┘└────┘  └┘   └┘  └─┘└──
typ  ───────┘└────┘ └┘ └┘└┘└┘└─┘└──
doc  ───────┘└────┘  └┘   └┘  └─┘└──
txt  ───────┘└────┘  └┘   └┘  └─┘└──
par  ───────┘└────┘  └┘   └┘  └─┘└──
pid  ─────────────┘  └┘   └┘  └─────
st   ───────────────────────────┘└─
347        let F := λx, some (Exy x),
id                      └──┘  └─┘
src  ─────┘└───────┘ └─┘└──┘     └─
typ  ─────┘└───────┘ └─┘└──┘ └─┘ └─
doc  ─────┘└───────┘ └─┘         └─
txt  ─────┘└───────┘ └─┘         └─
par  ─────┘└───────┘ └─┘         └─
pid  ──────────────┘ └─┘         └──
st   ──────────────────────────────┘└─
348        have Fspec : ∀x, F x ∈ s ∧ edist x (F x) < δ/2 := λx, some_spec (Exy x),
id                                   └───┘                    └───────┘  └─┘
src  ─────┘└───────────┘       └───┘    └┘   └───┘ └─┘└───────┘     └─
typ  ─────┘└───────────┘      └───┘   └┘  └───┘ └─┘└───────┘ └─┘ └─
doc  ─────┘└───────────┘                └┘   └───┘ └─┘              └─
txt  ─────┘└───────────┘                └┘   └───┘ └─┘              └─
par  ─────┘└───────────┘                └┘   └───┘ └─┘              └─
pid  ──────────────────┘                └┘   └───┘ └─┘              └──
st   ────────────────────────────────────────────────────────────────────────────┘└─
349  
src  
typ  
doc  
txt  
par  
pid  
st   
350        -- cover `t` with finitely many balls. Their centers form a set `a`
src  ──────────────────────────────────────────────────────────────────────────
typ  ──────────────────────────────────────────────────────────────────────────
doc  ──────────────────────────────────────────────────────────────────────────
txt  ──────────────────────────────────────────────────────────────────────────
par  ──────────────────────────────────────────────────────────────────────────
pid  ──────────────────────────────────────────────────────────────────────────
st   ──────────────────────────────────────────────────────────────────────────
351        have : totally_bounded t.val := (compact_iff_totally_bounded_complete.1 t.property.2).1,
id                └─────────────┘ └───┘     └──────────────────────────────────┘   └────────┘
src  ─────┘└─────┘└─────────────┘└───┘└──┘ └──────────────────────────────────┘└─┘└────────┘└───┘└─
typ  ─────┘└─────┘└─────────────┘└───┘└──┘ └──────────────────────────────────┘└─┘└────────┘└───┘└─
doc  ─────┘└─────┘└─────────────┘     └──┘                                     └─┘          └───┘└─
txt  ─────┘└─────┘                    └──┘                                     └─┘          └───┘└─
par  ─────┘└─────┘                    └──┘                                     └─┘          └───┘└─
pid  ────────────┘                    └──┘                                     └─┘          └──────
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
352        rcases totally_bounded_iff.1 this (δ/2) (ennreal.half_pos δpos) with ⟨a, af, ta⟩,
id                └─────────────────┘   └──┘       └──────────────┘ └──┘
src  ─────┘└─────┘└─────────────────┘└─┘       └─┘ └──────────────┘    └────────────────┘└─
typ  ─────┘└─────┘└─────────────────┘└─┘└──┘  └─┘ └──────────────┘└──┘└────────────────┘└─
doc  ─────┘└─────┘                   └─┘       └─┘                     └────────────────┘└─
txt  ─────┘└─────┘                   └─┘       └─┘                     └────────────────┘└─
par  ─────┘└─────┘                   └─┘       └─┘                     └────────────────┘└─
pid  ────────────┘                   └─┘       └─┘                     └───────────────────
st   ─────────────────────────────────────────────────────────────────────────────────────┘└─
353        -- a : set α,  af : finite a,  ta : t.val ⊆ ⋃ (y : α) (H : y ∈ a), eball y (δ / 2)
src  ─────────────────────────────────────────────────────────────────────────────────────────
typ  ─────────────────────────────────────────────────────────────────────────────────────────
doc  ─────────────────────────────────────────────────────────────────────────────────────────
txt  ─────────────────────────────────────────────────────────────────────────────────────────
par  ─────────────────────────────────────────────────────────────────────────────────────────
pid  ─────────────────────────────────────────────────────────────────────────────────────────
st   ─────────────────────────────────────────────────────────────────────────────────────────
354        -- replace each center by a nearby approximation in `s`, giving a new set `b`
src  ────────────────────────────────────────────────────────────────────────────────────
typ  ────────────────────────────────────────────────────────────────────────────────────
doc  ────────────────────────────────────────────────────────────────────────────────────
txt  ────────────────────────────────────────────────────────────────────────────────────
par  ────────────────────────────────────────────────────────────────────────────────────
pid  ────────────────────────────────────────────────────────────────────────────────────
st   ────────────────────────────────────────────────────────────────────────────────────
355        let b := F '' a,
id                      
src  ─────┘└───────┘    └─
typ  ─────┘└───────┘  └─
doc  ─────┘└───────┘    └─
txt  ─────┘└───────┘    └─
par  ─────┘└───────┘    └─
pid  ──────────────┘    └─
st   ────────────────────┘└─
356        have : finite b := finite_image _ af,
id                └────┘     └──────────┘   └┘
src  ─────┘└─────┘└────┘ └──┘└──────────┘└─┘  └─
typ  ─────┘└─────┘└────┘└──┘└──────────┘└─┘└┘└─
doc  ─────┘└─────┘└────┘ └──┘            └─┘  └─
txt  ─────┘└─────┘       └──┘            └─┘  └─
par  ─────┘└─────┘       └──┘            └─┘  └─
pid  ────────────┘       └──┘            └─┘  └─
st   ─────────────────────────────────────────┘└─
357        have tb : ∀x ∈ t.val, ∃y ∈ b, edist x y < δ,
id                        └───┘       └───┘       
src  ─────┘└────────┘ └──┘└───┘ └──┘ └───┘    └─
typ  ─────┘└────────┘ └──┘└───┘ └──┘└───┘   └─
doc  ─────┘└────────┘ └──┘       └──┘           └─
txt  ─────┘└────────┘ └──┘       └──┘           └─
par  ─────┘└────────┘ └──┘       └──┘           └─
pid  ───────────────┘ └──┘       └──┘           └─
st   ────────────────────────────────────────────────┘└─
358        { assume x hx,
src  ───────┘└─────────┘└─
typ  ───────┘└─────────┘└─
doc  ───────┘└─────────┘└─
txt  ───────┘└─────────┘└─
par  ───────┘└─────────┘└─
pid  ─────────────────────
st   ──────┘└──────────┘└─
359          rcases mem_bUnion_iff.1 (ta hx) with ⟨z, za, Dxz⟩,
id                  └────────────┘    └┘ └┘
src  ───────┘└─────┘└────────────┘└─┘     └─────────────────┘└─
typ  ───────┘└─────┘└────────────┘└─┘ └┘└┘└─────────────────┘└─
doc  ───────┘└─────┘              └─┘     └─────────────────┘└─
txt  ───────┘└─────┘              └─┘     └─────────────────┘└─
par  ───────┘└─────┘              └─┘     └─────────────────┘└─
pid  ──────────────┘              └─┘     └────────────────────
st   ────────────────────────────────────────────────────────┘└─
360          existsi [F z, mem_image_of_mem _ za],
id                       └──────────────┘   └┘
src  ───────┘└───────┘  └┘└──────────────┘└─┘  └─
typ  ───────┘└───────┘└┘└──────────────┘└─┘└┘└─
doc  ───────┘└───────┘  └┘                └─┘  └─
txt  ───────┘└───────┘  └┘                └─┘  └─
par  ───────┘└───────┘  └┘                └─┘  └─
pid  ────────────────┘  └┘                └─┘  └──
st   ───────────────────────────────────────────┘└─
361          calc edist x (F z) ≤ edist x z + edist z (F z) : edist_triangle _ _ _
id                                           └───┘          └────────────┘
src  ───────┘             └┘         └───┘    └──┘└────────────┘└──────
typ  ───────┘             └┘        └───┘   └──┘└────────────┘└──────
doc  ───────┘             └┘                  └──┘              └──────
txt  ───────┘             └┘                  └──┘              └──────
par  ───────┘             └┘                  └──┘              └──────
pid  ───────┘             └┘                  └──┘              └──────
st   ──────────────────────────────────────────────────────────────────────────────
362               ... < δ/2 + δ/2 : ennreal.add_lt_add Dxz (Fspec z).2
id                                 └────────────────┘ └─┘  └───┘ 
src  ────────────────┘   └┘  └──┘└────────────────┘          └───
typ  ────────────────┘   └┘  └──┘└────────────────┘└─┘ └───┘└───
doc  ────────────────┘   └┘   └──┘                            └───
txt  ────────────────┘   └┘   └──┘                            └───
par  ────────────────┘   └┘   └──┘                            └───
pid  ────────────────┘   └┘   └──┘                            └───
st   ──────────────────────────────────────────────────────────────────
363               ... = δ : ennreal.add_halves _ },
id                         └────────────────┘
src  ────────────────┘  └─┘└────────────────┘└─────
typ  ────────────────┘ └─┘└────────────────┘└─────
doc  ────────────────┘  └─┘                  └─────
txt  ────────────────┘  └─┘                  └─────
par  ────────────────┘  └─┘                  └─────
pid  ────────────────┘  └─┘                  └─────
st   ──────────────────────────────────────────┘└┘└─
364        -- keep only the points in `b` that are close to point in `t`, yielding a new set `c`
src  ────────────────────────────────────────────────────────────────────────────────────────────
typ  ────────────────────────────────────────────────────────────────────────────────────────────
doc  ────────────────────────────────────────────────────────────────────────────────────────────
txt  ────────────────────────────────────────────────────────────────────────────────────────────
par  ────────────────────────────────────────────────────────────────────────────────────────────
pid  ────────────────────────────────────────────────────────────────────────────────────────────
st   ────────────────────────────────────────────────────────────────────────────────────────────
365        let c := {y ∈ b | ∃x∈t.val, edist x y < δ},
id                           └───┘ └───┘       
src  ─────┘└───────┘└──┘ └─┘└┘└───┘└───┘    └─
typ  ─────┘└───────┘└──┘└─┘└┘└───┘└───┘   └─
doc  ─────┘└───────┘ └──┘ └─┘ └┘               └─
txt  ─────┘└───────┘ └──┘ └─┘ └┘               └─
par  ─────┘└───────┘ └──┘ └─┘ └┘               └─
pid  ──────────────┘ └──┘ └─┘ └┘               └──
st   ───────────────────────────────────────────────┘└─
366        have : finite c := finite_subset ‹finite b› (λx hx, hx.1),
id                └────┘     └───────────┘ └────┘ 
src  ─────┘└─────┘└────┘ └──┘└───────────┘└────┘   └────┘  └─┘└─
typ  ─────┘└─────┘└────┘└──┘└───────────┘└────┘  └────┘  └─┘└─
doc  ─────┘└─────┘└────┘ └──┘             └────┘   └────┘  └─┘└─
txt  ─────┘└─────┘       └──┘                        └────┘  └─┘└─
par  ─────┘└─────┘       └──┘                        └────┘  └─┘└─
pid  ────────────┘       └──┘                        └────┘  └────
st   ──────────────────────────────────────────────────────────────┘└─
367        -- points in `t` are well approximated by points in `c`
src  ──────────────────────────────────────────────────────────────
typ  ──────────────────────────────────────────────────────────────
doc  ──────────────────────────────────────────────────────────────
txt  ──────────────────────────────────────────────────────────────
par  ──────────────────────────────────────────────────────────────
pid  ──────────────────────────────────────────────────────────────
st   ──────────────────────────────────────────────────────────────
368        have tc : ∀x ∈ t.val, ∃y ∈ c, edist x y ≤ δ,
id                        └───┘       └───┘      
src  ─────┘└────────┘ └──┘└───┘ └──┘ └───┘   └─
typ  ─────┘└────────┘ └──┘└───┘ └──┘└───┘  └─
doc  ─────┘└────────┘ └──┘       └──┘           └─
txt  ─────┘└────────┘ └──┘       └──┘           └─
par  ─────┘└────────┘ └──┘       └──┘           └─
pid  ───────────────┘ └──┘       └──┘           └─
st   ────────────────────────────────────────────────┘└─
369        { assume x hx,
src  ───────┘└─────────┘└─
typ  ───────┘└─────────┘└─
doc  ───────┘└─────────┘└─
txt  ───────┘└─────────┘└─
par  ───────┘└─────────┘└─
pid  ─────────────────────
st   ──────┘└──────────┘└─
370          rcases tb x hx with ⟨y, yv, Dxy⟩,
id                  └┘  └┘
src  ───────┘└─────┘     └────────────────┘└─
typ  ───────┘└─────┘└┘└┘└────────────────┘└─
doc  ───────┘└─────┘     └────────────────┘└─
txt  ───────┘└─────┘     └────────────────┘└─
par  ───────┘└─────┘     └────────────────┘└─
pid  ──────────────┘     └───────────────────
st   ───────────────────────────────────────┘└─
371          have : y ∈ c := by simp [c, -mem_image]; exact ⟨yv, ⟨x, hx, Dxy⟩⟩,
id                                                        └┘     └┘  └─┘
src  ───────┘└─────┘   └──┘  └────┘ └───────────┘└┘└────┘   └┘  └┘  └┘   └┘└─
typ  ───────┘└─────┘ └──┘  └────┘└───────────┘└┘└────┘ └┘└┘ └┘└┘└┘└─┘└┘└─
doc  ───────┘└─────┘   └──┘  └────┘ └───────────┘└┘└────┘   └┘  └┘  └┘   └┘└─
txt  ───────┘└─────┘   └──┘  └────┘ └───────────┘└┘└────┘   └┘  └┘  └┘   └┘└─
par  ───────┘└─────┘   └──┘  └────┘ └───────────┘└┘└────┘   └┘  └┘  └┘   └┘└─
pid  ──────────────┘   └──┘  └─────┘ └───────────────────┘   └┘  └┘  └┘   └───
st   ─────────────────────────┘└─────────────────────────────────────────────┘└─
372          exact ⟨y, this, le_of_lt Dxy⟩ },
id                    └──┘  └──────┘ └─┘
src  ───────┘└────┘  └┘    └┘└──────┘   └┘└──
typ  ───────┘└────┘ └┘└──┘└┘└──────┘└─┘└┘└──
doc  ───────┘└────┘  └┘    └┘           └┘└──
txt  ───────┘└────┘  └┘    └┘           └┘└──
par  ───────┘└────┘  └┘    └┘           └┘└──
pid  ─────────────┘  └┘    └┘           └────
st   ─────────────────────────────────────┘└─
373        -- points in `c` are well approximated by points in `t`
src  ──────────────────────────────────────────────────────────────
typ  ──────────────────────────────────────────────────────────────
doc  ──────────────────────────────────────────────────────────────
txt  ──────────────────────────────────────────────────────────────
par  ──────────────────────────────────────────────────────────────
pid  ──────────────────────────────────────────────────────────────
st   ──────────────────────────────────────────────────────────────
374        have ct : ∀y ∈ c, ∃x ∈ t.val, edist y x ≤ δ,
id                              └───┘ └───┘       
src  ─────┘└────────┘ └──┘  └──┘└───┘└───┘    └─
typ  ─────┘└────────┘ └──┘ └──┘└───┘└───┘   └─
doc  ─────┘└────────┘ └──┘   └──┘               └─
txt  ─────┘└────────┘ └──┘   └──┘               └─
par  ─────┘└────────┘ └──┘   └──┘               └─
pid  ───────────────┘ └──┘   └──┘               └─
st   ────────────────────────────────────────────────┘└─
375        { rintros y ⟨hy1, ⟨x, xt, Dyx⟩⟩,
src  ───────┘└───────────────────────────┘└─
typ  ───────┘└───────────────────────────┘└─
doc  ───────┘└───────────────────────────┘└─
txt  ───────┘└───────────────────────────┘└─
par  ───────┘└───────────────────────────┘└─
pid  ───────────────────────────────────────
st   ──────┘└────────────────────────────┘└─
376          have : edist y x ≤ δ := calc
id                  └───┘     
src  ───────┘└─────┘└───┘    └──┘    
typ  ───────┘└─────┘└───┘ └──┘    
doc  ───────┘└─────┘         └──┘    
txt  ───────┘└─────┘         └──┘    
par  ───────┘└─────┘         └──┘    
pid  ──────────────┘         └──┘    
st   ─────────────────────────────────────
377            edist y x = edist x y : edist_comm _ _
id                         └───┘     └────────┘
src  ─────────┘        └───┘  └─┘└────────┘└────
typ  ─────────┘        └───┘└─┘└────────┘└────
doc  ─────────┘               └─┘          └────
txt  ─────────┘               └─┘          └────
par  ─────────┘               └─┘          └────
pid  ─────────┘               └─┘          └────
st   ─────────────────────────────────────────────────
378            ... ≤ δ : le_of_lt Dyx,
id                      └──────┘ └─┘
src  ─────────────┘  └─┘└──────┘   └─
typ  ─────────────┘ └─┘└──────┘└─┘└─
doc  ─────────────┘  └─┘           └─
txt  ─────────────┘  └─┘           └─
par  ─────────────┘  └─┘           └─
pid  ─────────────┘  └─┘           └─
st   ───────────────────────────────┘└─
379          exact ⟨x, xt, this⟩ },
id                    └┘  └──┘
src  ───────┘└────┘  └┘  └┘    └┘└──
typ  ───────┘└────┘ └┘└┘└┘└──┘└┘└──
doc  ───────┘└────┘  └┘  └┘    └┘└──
txt  ───────┘└────┘  └┘  └┘    └┘└──
par  ───────┘└────┘  └┘  └┘    └┘└──
pid  ─────────────┘  └┘  └┘    └────
st   ───────────────────────────┘└─
380        -- it follows that their Hausdorff distance is small
src  ───────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────
381        have : Hausdorff_edist t.val c ≤ δ :=
id                └─────────────┘ └───┘    
src  ─────┘└─────┘└─────────────┘└───┘   └───
typ  ─────┘└─────┘└─────────────┘└───┘ └───
doc  ─────┘└─────┘└─────────────┘        └───
txt  ─────┘└─────┘                       └───
par  ─────┘└─────┘                       └───
pid  ────────────┘                       └───
st   ────────────────────────────────────────────
382          Hausdorff_edist_le_of_mem_edist tc ct,
id           └─────────────────────────────┘ └┘ └┘
src  ───────┘└─────────────────────────────┘└┘  └─
typ  ───────┘└─────────────────────────────┘└┘└┘└─
doc  ───────┘└─────────────────────────────┘    └─
txt  ───────┘                                   └─
par  ───────┘                                   └─
pid  ───────┘                                   └─
st   ────────────────────────────────────────────┘└─
383        have Dtc : Hausdorff_edist t.val c < ε := lt_of_le_of_lt this δlt,
id                    └─────────────┘ └───┘        └────────────┘ └──┘ └─┘
src  ─────┘└─────────┘└─────────────┘└───┘   └──┘└────────────┘       └─
typ  ─────┘└─────────┘└─────────────┘└───┘ └──┘└────────────┘└──┘└─┘└─
doc  ─────┘└─────────┘└─────────────┘        └──┘                     └─
txt  ─────┘└─────────┘                       └──┘                     └─
par  ─────┘└─────────┘                       └──┘                     └─
pid  ────────────────┘                       └──┘                     └─
st   ──────────────────────────────────────────────────────────────────────┘└─
384        -- the set `c` is not empty, as it is well approximated by a nonempty set
src  ────────────────────────────────────────────────────────────────────────────────
typ  ────────────────────────────────────────────────────────────────────────────────
doc  ────────────────────────────────────────────────────────────────────────────────
txt  ────────────────────────────────────────────────────────────────────────────────
par  ────────────────────────────────────────────────────────────────────────────────
pid  ────────────────────────────────────────────────────────────────────────────────
st   ────────────────────────────────────────────────────────────────────────────────
385        have hc : c.nonempty,
id                   └────────┘
src  ─────┘└────────┘└────────┘└─
typ  ─────┘└────────┘└────────┘└─
doc  ─────┘└────────┘└────────┘└─
txt  ─────┘└────────┘          └─
par  ─────┘└────────┘          └─
pid  ───────────────┘          └─
st   ─────────────────────────┘└─
386          from nonempty_of_Hausdorff_edist_ne_top t.property.1 (lattice.ne_top_of_lt Dtc),
id                └────────────────────────────────┘ └────────┘    └──────────────────┘ └─┘
src  ───────┘└───┘└────────────────────────────────┘└────────┘└─┘ └──────────────────┘   └─
typ  ───────┘└───┘└────────────────────────────────┘└────────┘└─┘ └──────────────────┘└─┘└─
doc  ───────┘└───┘└────────────────────────────────┘          └─┘                        └─
txt  ───────┘└───┘                                            └─┘                        └─
par  ───────┘└───┘                                            └─┘                        └─
pid  ────────────┘                                            └─┘                        └──
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
387        -- let `d` be the version of `c` in the type `nonempty_compacts α`
src  ─────────────────────────────────────────────────────────────────────────
typ  ─────────────────────────────────────────────────────────────────────────
doc  ─────────────────────────────────────────────────────────────────────────
txt  ─────────────────────────────────────────────────────────────────────────
par  ─────────────────────────────────────────────────────────────────────────
pid  ─────────────────────────────────────────────────────────────────────────
st   ─────────────────────────────────────────────────────────────────────────
388        let d : nonempty_compacts α := ⟨c, ⟨hc, ‹finite c›.compact⟩⟩,
id                 └───────────────┘          └┘   └────┘ 
src  ─────┘└──────┘└───────────────┘ └──┘  └┘   └┘ └────┘  └────────┘└─
typ  ─────┘└──────┘└───────────────┘└──┘  └┘ └┘└┘ └────┘ └────────┘└─
doc  ─────┘└──────┘└───────────────┘ └──┘  └┘   └┘ └────┘  └────────┘└─
txt  ─────┘└──────┘                  └──┘  └┘   └┘         └────────┘└─
par  ─────┘└──────┘                  └──┘  └┘   └┘         └────────┘└─
pid  ─────────────┘                  └──┘  └┘   └┘         └───────────
st   ─────────────────────────────────────────────────────────────────┘└─
389        have : c ⊆ s,
id                   
src  ─────┘└─────┘   └─
typ  ─────┘└─────┘ └─
doc  ─────┘└─────┘   └─
txt  ─────┘└─────┘   └─
par  ─────┘└─────┘   └─
pid  ────────────┘   └─
st   ─────────────────┘└─
390        { assume x hx,
src  ───────┘└─────────┘└─
typ  ───────┘└─────────┘└─
doc  ───────┘└─────────┘└─
txt  ───────┘└─────────┘└─
par  ───────┘└─────────┘└─
pid  ─────────────────────
st   ──────┘└──────────┘└─
391          rcases (mem_image _ _ _).1 hx.1 with ⟨y, ⟨ya, yx⟩⟩,
id                   └───────┘          └┘
src  ───────┘└─────┘ └───────┘└────────┘  └───────────────────┘└─
typ  ───────┘└─────┘ └───────┘└────────┘└┘└───────────────────┘└─
doc  ───────┘└─────┘          └────────┘  └───────────────────┘└─
txt  ───────┘└─────┘          └────────┘  └───────────────────┘└─
par  ───────┘└─────┘          └────────┘  └───────────────────┘└─
pid  ──────────────┘          └────────┘  └──────────────────────
st   ─────────────────────────────────────────────────────────┘└─
392          rw ← yx,
id                └┘
src  ───────┘└───┘  └─
typ  ───────┘└───┘└┘└─
doc  ───────┘└───┘  └─
txt  ───────┘└───┘  └─
par  ───────┘└───┘  └─
pid  ────────────┘  └─
st   ──────────────┘└─
393          exact (Fspec y).1 },
id                  └───┘ 
src  ───────┘└────┘       └──┘└──
typ  ───────┘└────┘ └───┘└──┘└──
doc  ───────┘└────┘       └──┘└──
txt  ───────┘└────┘       └──┘└──
par  ───────┘└────┘       └──┘└──
pid  ─────────────┘       └──────
st   ─────────────────────────┘└─
394        have : d ∈ v := ⟨‹finite c›, this⟩,
id                         └────┘    └──┘
src  ─────┘└─────┘   └──┘  └────┘  └┘    └─
typ  ─────┘└─────┘ └──┘  └────┘ └┘└──┘└─
doc  ─────┘└─────┘   └──┘  └────┘  └┘    └─
txt  ─────┘└─────┘   └──┘          └┘    └─
par  ─────┘└─────┘   └──┘          └┘    └─
pid  ────────────┘   └──┘          └┘    └──
st   ───────────────────────────────────────┘└─
395        -- we have proved that `d` is a good approximation of `t` as requested
src  ─────────────────────────────────────────────────────────────────────────────
typ  ─────────────────────────────────────────────────────────────────────────────
doc  ─────────────────────────────────────────────────────────────────────────────
txt  ─────────────────────────────────────────────────────────────────────────────
par  ─────────────────────────────────────────────────────────────────────────────
pid  ─────────────────────────────────────────────────────────────────────────────
st   ─────────────────────────────────────────────────────────────────────────────
396        exact ⟨d, ‹d ∈ v›, Dtc⟩ },
id                          └─┘
src  ─────┘└────┘  └┘     └┘   └┘└──
typ  ─────┘└────┘  └┘   └┘└─┘└┘└──
doc  ─────┘└────┘  └┘     └┘   └┘└──
txt  ─────┘└────┘  └┘     └┘   └┘└──
par  ─────┘└────┘  └┘     └┘   └┘└──
pid  ───────────┘  └┘     └┘   └────
st   ─────────────────────────────┘└──
397    end,
src  ────┘
typ  ────┘
doc  ────┘
txt  ────┘
par  ────┘
pid  ────┘
st   ────┘└─
398    apply second_countable_of_separable,
id           └───────────────────────────┘
src    └────┘└───────────────────────────┘
typ    └────┘└───────────────────────────┘
doc    └────┘└───────────────────────────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────────────────────────┘└─
399  end
st   ──┘
400  
401  end --section
402  end emetric --namespace
403  
404  namespace metric
405  section
406  
407  variables {α : Type u} [metric_space α]
id                           └──────────┘
src                          └──────────┘
typ                          └──────────┘
doc                          └──────────┘
408  
409  /-- `nonempty_compacts α` inherits a metric space structure, as the Hausdorff
410  edistance between two such sets is finite. -/
411  instance nonempty_compacts.metric_space : metric_space (nonempty_compacts α) :=
id                                             └──────────┘  └───────────────┘ 
src                                            └──────────┘  └───────────────┘
typ                                            └──────────┘  └───────────────┘ 
doc                                            └──────────┘  └───────────────┘
412  emetric_space.to_metric_space $ λx y, Hausdorff_edist_ne_top_of_nonempty_of_bounded x.2.1 y.2.1
id   └───────────────────────────┘       └───────────────────────────────────────────┘     
src  └───────────────────────────┘         └───────────────────────────────────────────┘       
typ  └───────────────────────────┘       └───────────────────────────────────────────┘     
doc  └───────────────────────────┘         └───────────────────────────────────────────┘
413    (bounded_of_compact x.2.2) (bounded_of_compact y.2.2)
id      └────────────────┘      └────────────────┘  
src     └────────────────┘       └────────────────┘   
typ     └────────────────┘      └────────────────┘  
doc     └────────────────┘         └────────────────┘
414  
415  /-- The distance on `nonempty_compacts α` is the Hausdorff distance, by construction -/
416  lemma nonempty_compacts.dist_eq {x y : nonempty_compacts α} :
id                                          └───────────────┘ 
src                                         └───────────────┘
typ                                         └───────────────┘ 
doc                                         └───────────────┘
417    dist x y = Hausdorff_dist x.val y.val := rfl
id     └──┘    └────────────┘ └──┘ └──┘    └─┘
src    └──┘      └────────────┘  └──┘  └──┘    └─┘
typ    └──┘    └────────────┘ └──┘ └──┘    └─┘
doc               └────────────┘
418  
419  lemma lipschitz_inf_dist_set (x : α) :
id                                     
typ                                    
420    lipschitz_with 1 (λ s : nonempty_compacts α, inf_dist x s.val) :=
id     └────────────┘          └───────────────┘   └──────┘  └──┘
src    └────────────┘          └───────────────┘    └──────┘    └──┘
typ    └────────────┘          └───────────────┘   └──────┘  └──┘
doc    └────────────┘          └───────────────┘    └──────┘
421  lipschitz_with.one_of_le_add $ assume s t,
id   └──────────────────────────┘           
src  └──────────────────────────┘
typ  └──────────────────────────┘           
422  by { rw dist_comm,
id           └───────┘
src       └─┘└───────┘
typ       └─┘└───────┘
doc       └─┘
txt       └─┘
par       └─┘
pid         
st     └─────────────┘└─
423    exact inf_dist_le_inf_dist_add_Hausdorff_dist (edist_ne_top t s) }
id           └─────────────────────────────────────┘  └──────────┘  
src    └────┘└─────────────────────────────────────┘ └──────────┘  └┘
typ    └────┘└─────────────────────────────────────┘ └──────────┘└┘
doc    └────┘└─────────────────────────────────────┘ └──────────┘  └┘
txt    └────┘                                                      └┘
par    └────┘                                                      └┘
pid                                                               
st   ──────────────────────────────────────────────────────────────────┘└┘
424  
425  lemma lipschitz_inf_dist :
426    lipschitz_with 2 (λ p : α × (nonempty_compacts α), inf_dist p.1 p.2.val) :=
id     └────────────┘             └───────────────┘    └──────┘    └─┘
src    └────────────┘              └───────────────┘     └──────┘      └─┘
typ    └────────────┘             └───────────────┘    └──────┘    └─┘
doc    └────────────┘               └───────────────┘     └──────┘
427  @lipschitz_with.uncurry' _ _ _ _ _ _ (λ (x : α) (s : nonempty_compacts α), inf_dist x s.val) 1 1
id    └─────────────────────┘                            └───────────────┘    └──────┘  └──┘
src   └─────────────────────┘                             └───────────────┘     └──────┘    └──┘
typ   └─────────────────────┘                            └───────────────┘    └──────┘  └──┘
doc                                                       └───────────────┘     └──────┘
428    (λ s, lipschitz_inf_dist_pt s.val) lipschitz_inf_dist_set
id          └───────────────────┘ └──┘  └────────────────────┘
src          └───────────────────┘  └──┘  └────────────────────┘
typ         └───────────────────┘ └──┘  └────────────────────┘
doc          └───────────────────┘
429  
430  lemma uniform_continuous_inf_dist_Hausdorff_dist :
431    uniform_continuous (λp : α × (nonempty_compacts α), inf_dist p.1 (p.2).val) :=
id     └────────────────┘          └───────────────┘    └──────┘      └─┘
src    └────────────────┘           └───────────────┘     └──────┘        └─┘
typ    └────────────────┘          └───────────────┘    └──────┘      └─┘
doc                                  └───────────────┘     └──────┘
432  lipschitz_inf_dist.to_uniform_continuous
id   └────────────────┘└────────────────────┘
src  └────────────────┘└────────────────────┘
typ  └────────────────┘└────────────────────┘
doc                    └────────────────────┘
433  
434  end --section
435  end metric --namespace